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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-10 15:06:03 -08:00
parent a28ff92010
commit 762b0f42ba
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/letRecMissingAnnotation.lean.expected.out
View file

@ -1,4 +1,4 @@
letRecMissingAnnotation.lean:4:6-4:34: error: unsolved goals
letRecMissingAnnotation.lean:4:6-4:34: error: tactic 'assumption' failed,
as : Array Nat
i s : Nat
h : i < Array.size as

2
tests/lean/wf2.lean.expected.out
View file

@ -1,3 +1,3 @@
wf2.lean:3:8-3:17: error: unsolved goals
wf2.lean:3:8-3:17: error: tactic 'assumption' failed,
x y : Nat
⊢ x - 1 < x