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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
(**********************************************************************)
(* Notations for if and let (submitted by Roland Zumkeller) *)
Notation "a ? b ; c" := (if a then b else c) (at level 10).
Check (true ? 0 ; 1).
Check if true as x return (if x then nat else bool) then 0 else true.
Notation "'proj1' t" := (let (a,_) := t in a) (at level 1).
Check (fun e : nat * nat => proj1 e).
Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1).
Check (decomp (true,true) as t, u in (t,u)).
(**********************************************************************)
(* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
Section A.
Notation "! A" := (forall _:nat, A) (at level 60).
Check ! (0=0).
Check forall n, n=0.
Check forall n:nat, 0=0.
End A.
(**********************************************************************)
(* Behaviour wrt to binding variables (cf bug report #1186) *)
Section B.
Notation "# A" := (forall n:nat, n=n->A) (at level 60).
Check forall n:nat, # (n=n).
Notation "## A" := (forall n n0:nat, n=n0->A) (at level 60).
Check forall n n0:nat, ## (n=n0).
Notation "### A" :=
(forall n n0:nat, match n with O => True | S n => n=n0 end ->A) (at level 60).
Check forall n n0:nat, ### (n=n0).
End B.
(**********************************************************************)
(* Conflict between notation and notation below coercions *)
(* Case of a printer conflict *)
Require Import BinInt.
Coercion Zpos : positive >-> Z.
Open Scope Z_scope.
(* Check that (Zpos 3) is better printed by the printer for Z than
by the printer for positive *)
Check (3 + Zpos 3).
(* Case of a num printer only below coercion (submitted by Georges Gonthier) *)
Open Scope nat_scope.
Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
Coercion Zpos: nat >-> znat.
Delimit Scope znat_scope with znat.
Open Scope znat_scope.
Variable addz : znat -> znat -> znat.
Notation "z1 + z2" := (addz z1 z2) : znat_scope.
(* Check that "3+3", where 3 is in nat and the coercion to znat is implicit,
is printed the same way, and not "S 2 + S 2" as if numeral printing was
only tested with coercion still present *)
Check (3+3).
(**********************************************************************)
(* Check recursive notations *)
Require Import List.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Check [1;2;4].
Reserved Notation "( x ; y , .. , z )" (at level 0).
Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
Check (1;2,4).
(* Check basic notations involving "match" *)
Section C.
Notation "'ifzero' n" := (match n with 0 => true | S _ => false end)
(at level 0, n at level 0).
Check (ifzero 3).
Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end)
(at level 0, n at level 0).
Check (pred 3).
Check (fun n => match n with 0 => 0 | S n => n end).
Check (fun n => match n with S p as x => p | y => 0 end).
Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" :=
(match x with O => u | S n => t end) (at level 0, u at level 0).
Check fun x => ifn x is succ n then n else 0.
End C.
(* Check correction of bug #1179 *)
Notation "1 -" := true (at level 0).
Check 1-.
(* This is another aspect of bug #1179 (raises anomaly in 8.1) *)
Require Import ZArith.
Open Scope Z_scope.
Notation "- 4" := (-2 + -2).
Check -4.
(**********************************************************************)
(* Check preservation of scopes at printing time *)
Notation SUM := sum.
Check SUM (nat*nat) nat.
(**********************************************************************)
(* Check preservation of implicit arguments at printing time *)
Notation FST := fst.
Check FST (0;1).
(**********************************************************************)
(* Check notations for references with activated or deactivated *)
(* implicit arguments *)
Notation Nil := @nil.
Check Nil.
Notation NIL := nil.
Check NIL : list nat.
(**********************************************************************)
(* Test printing of notation with coercions in scope of a coercion *)
Open Scope nat_scope.
Coercion is_true := fun b => b=true.
Coercion of_nat n := match n with 0 => true | _ => false end.
Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
Check (false && I 3)%bool /\ I 6.
(**********************************************************************)
(* Check notations with several recursive patterns *)
Open Scope Z_scope.
Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
(pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
Check [|1,2,3;4,5,6|].
(**********************************************************************)
(* Test recursive notations involving applications *)
(* Caveat: does not work for applied constant because constants are *)
(* classified as notations for the particular constant while this *)
(* generic application notation is classified as generic *)
Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
Check fun f => {| f; 0; 1; 2 |} : Z.
(**********************************************************************)
(* Check printing of notations from other modules *)
(* 1- Non imported case *)
Require make_notation.
Check plus.
Check S.
Check mult.
Check le.
(* 2- Imported case *)
Import make_notation.
Check plus.
Check S.
Check mult.
Check le.
(* Check notations in cases patterns *)
Notation SOME := Some.
Notation NONE := None.
Check (fun x => match x with SOME x => x | NONE => 0 end).
Notation NONE2 := (@None _).
Notation SOME2 := (@Some _).
Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
Notation NONE3 := @None.
Notation SOME3 := @Some.
Check (fun x => match x with SOME3 x => x | NONE3 => 0 end).
|
