blob: ee5446e54818479c50dda9841d1a240842829361 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* A wish granted by the new support for patterns in notations *)
Local Notation mkmatch0 e p
:= match e with
| p => true
| _ => false
end.
Local Notation "'mkmatch' [[ e ]] [[ p ]]"
:= match e with
| p => true
| _ => false
end
(at level 0, p pattern).
Check mkmatch0 _ ((0, 0)%core).
Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]].
|
