1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
(* An example with constr subentries *)
Module A.
Declare Custom Entry myconstr.
Notation "[ x ]" := x (x custom myconstr at level 6).
Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope.
Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope.
Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
Check [ < 0 > + < 1 > * < 2 >].
Axiom a : nat.
Notation b := a.
Check [ < b > + < a > * < 2 >].
Declare Custom Entry anotherconstr.
Notation "[ x ]" := x (x custom myconstr at level 6).
Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr at level 10).
Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
Check [ << # 0 >> ].
End A.
Module B.
Inductive Expr :=
| Mul : Expr -> Expr -> Expr
| Add : Expr -> Expr -> Expr
| One : Expr.
Declare Custom Entry expr.
Notation "[ expr ]" := expr (expr custom expr at level 2).
Notation "1" := One (in custom expr at level 0).
Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity).
Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
Notation "( x )" := x (in custom expr at level 0, x at level 2).
Notation "{ x }" := x (in custom expr at level 0, x constr).
Notation "x" := x (in custom expr at level 0, x ident).
Axiom f : nat -> Expr.
Check [1 {f 1}].
Check fun x y z => [1 + y z + {f x}].
Check fun e => match e with
| [x y + z] => [x + y z]
| [1 + 1] => [1]
| y => [y + e]
end.
End B.
Module C.
Inductive Expr :=
| Add : Expr -> Expr -> Expr
| One : Expr.
Declare Custom Entry expr.
Notation "[ expr ]" := expr (expr custom expr at level 1).
Notation "1" := One (in custom expr at level 0).
Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
Notation "( x )" := x (in custom expr at level 0, x at level 2).
(* Check the use of a two-steps coercion from constr to expr 1 then
from expr 0 to expr 2 (note that camlp5 parsing is more tolerant
and does not require parentheses to parse from level 2 while at
level 1) *)
Check [1 + 1].
End C.
(* An example of interaction between coercion and notations from
Robbert Krebbers. *)
Require Import String.
Module D.
Inductive expr :=
| Var : string -> expr
| Lam : string -> expr -> expr
| App : expr -> expr -> expr.
Notation Let x e1 e2 := (App (Lam x e2) e1).
Parameter e1 e2 : expr.
Check (Let "x" e1 e2).
Coercion App : expr >-> Funclass.
Check (Let "x" e1 e2).
End D.
(* Check fix of #8551: a delimiter should be inserted because the
lonely notation hides the scope nat_scope, even though the latter
is open *)
Module E.
Notation "# x" := (S x) (at level 20) : nat_scope.
Notation "# x" := (Some x).
Check fun x => (# x)%nat.
End E.
(* Other tests of precedence *)
Module F.
Notation "# x" := (S x) (at level 20) : nat_scope.
Notation "## x" := (S x) (at level 20).
Check fun x => S x.
Open Scope nat_scope.
Check fun x => S x.
Notation "### x" := (S x) (at level 20) : nat_scope.
Check fun x => S x.
Close Scope nat_scope.
Check fun x => S x.
End F.
(* Lower priority of generic application rules *)
Module G.
Declare Scope predecessor_scope.
Delimit Scope predecessor_scope with pred.
Declare Scope app_scope.
Delimit Scope app_scope with app.
Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope.
Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope.
Check fun x => pred x.
End G.
(* Checking arbitration between in the presence of a notation in type scope *)
Module H.
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity,
format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope.
Check forall a, a = 0.
Close Scope type_scope.
Check ((forall a, a = 0) -> True)%type.
Open Scope type_scope.
Notation "#" := (forall a, a = 0).
Check #.
Check # -> True.
Close Scope type_scope.
Check (# -> True)%type.
Open Scope type_scope.
Declare Scope my_scope.
Notation "##" := (forall a, a = 0) : my_scope.
Open Scope my_scope.
Check ##.
End H.
|
