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
|
Declare Custom Entry expr.
Check fun expr => expr.
Check fun constr => constr.
Goal True.
let x := open_constr:(1+1) in pose x.
let x := constr:(1+1) in pose x.
Abort.
Module A.
Notation "'constr' : ( e )" := e (in custom expr, e constr).
Notation "'expr' : ( e )" := e (e custom expr).
Check expr:( constr:( 1 )).
Check fun expr => expr.
Check fun constr => constr.
Goal True.
let x := open_constr:(1+1) in pose x.
let x := constr:(1+1) in pose x.
Abort.
End A.
Module B.
Notation "'expr' : ( e )" := e (e custom expr).
Notation "'constr' : ( e )" := e (in custom expr, e constr).
Check expr:( constr:( 1 )).
Check fun expr => expr.
Check fun constr => constr.
Goal True.
let x := open_constr:(1+1) in pose x.
let x := constr:(1+1) in pose x.
Abort.
End B.
|
