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
|
Declare Scope blafu.
Delimit Scope blafu with B.
Axiom DoesNotMatch : Type.
Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit.
Notation "| p1 | .. | pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu.
Notation "'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" :=
(@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
(at level 200, ls at level 91, only parsing).
Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
(mmatch_do_not_write x in T as y return M p with_do_not_write ls)
(at level 200, ls at level 91, p at level 10, only parsing).
(* This should not gives a warning *)
Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
(@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
(at level 200, ls at level 91, p at level 10, only printing,
format "'[ ' mmatch '/' x ']' '/' '[ ' in '/' T ']' '/' '[ ' as '/' y ']' '/' '[ ' return M p ']' with '//' '[' ls ']' '//' end"
).
(* Check use of "mmatch" *)
Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end).
(* 2nd example *)
Notation "#" := I (at level 0, only parsing).
Notation "#" := I (at level 0, only printing).
Check #.
Notation "##" := I (at level 0, only printing).
Notation "##" := I (at level 0, only parsing).
Check ##.
|
