1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Declare Custom Entry foo.
Declare Custom Entry bar.
Parameter (A : Type).
Parameter (Q : A -> A -> A).
Parameter (P : A -> A).
Notation "< x >" := (P x) (x custom foo).
Notation "x y" := (Q x y) (in custom bar at level 1, right associativity).
Notation "x" := x (in custom bar at level 0, x global).
Module Order1.
Notation "| x |" := (x) (x custom bar).
Notation "{ x }" := (x) (in custom foo, x constr).
Check (fun a b => < {Q b a} >).
End Order1.
Module Order2.
Notation "{ x }" := (x) (in custom foo, x constr).
Notation "| x |" := (x) (x custom bar).
Check (fun a b => < {Q b a} >).
End Order2.
|
