1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Declare Custom Entry expr.
Declare Custom Entry stmt.
Notation "x" := x (in custom stmt, x ident).
Notation "x" := x (in custom expr, x ident).
Notation "'_'" := _ (in custom expr).
Notation "1" := 1 (in custom expr).
Notation "! x = y !" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
Notation "? x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
Notation "x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
Notation "stmt:( s )" := s (s custom stmt).
Check stmt:(! _ = _ !).
Check stmt:(? _ = _).
Check stmt:(_ = _).
Check stmt:(! 1 = 1 !).
Check stmt:(? 1 = 1).
Check stmt:(1 = 1).
Check stmt:(_ = 1).
|
