blob: 2c6d391a0c539d1129b5bfa5bef361bd7febb2d4 (
plain)
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
|
Module a.
Fail Check let x' := _ in
$(exact x')$.
Notation foo x := (let x' := x in $(exact x')$).
Fail Check foo _. (* Error:
Cannot infer an internal placeholder of type "Type" in environment:
x' := ?42 : ?41
. *)
End a.
Module b.
Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I).
Notation bar x := (let x' := x in let y := (I : True) in I).
Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *)
Check bar _. (* let x' := ?9 in let y := I in I *)
Fail Check foo _. (* Error:
Cannot infer an internal placeholder of type "Type" in environment:
x' := ?42 : ?41
. *)
End b.
|
