blob: 19e306fea800433da265abe8ada88ee9e1deeffc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Check correct separation of identifiers followed by unicode symbols *)
Notation "x 〈 w" := (plus x w) (at level 30).
Check fun x => x〈x.
(* Check Greek letters *)
Definition test_greek : nat -> nat := fun Δ => Δ.
Parameter ℝ : Set.
Parameter π : ℝ.
(* Check indices *)
Definition test_indices : nat -> nat := fun x₁ => x₁.
Definition π₂ := snd.
|
