max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: add another missing hole test

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-07 17:18:20 -07:00
parent fc0be5e391
commit ef87b33cdc
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/holes.lean
View file

@ -20,3 +20,7 @@ f a
partial def f7 (x : Nat) :=
f7 x
partial def f8 (x : Nat) :=
let rec aux (y : Nat) := aux y;
x + 1

5
tests/lean/holes.lean.expected.out
View file

@ -49,3 +49,8 @@ holes.lean:21:25: error: don't know how to synthesize placeholder
context:
x : Nat
⊢ Sort ?
holes.lean:25:8: error: don't know how to synthesize placeholder
context:
f8 : Nat → Nat
x y : Nat
⊢ Sort ?