blob: ced535afd50a50466e8fe38d574d5796293613d5 (
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.
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.
|
