blob: e3c4dd300d590548a2858f78077de916e5832f5c (
plain)
1
2
3
4
5
6
7
8
9
|
(* 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 Δ => Δ.
(* Check indices *)
Definition test_indices : nat -> nat := fun x₁ => x₁.
|
