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

test: fix beginEndAsMacro output

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-09 19:33:11 +01:00
parent 5673702687
commit a6fca7bced
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,3 +1,3 @@
beginEndAsMacro.lean:21:2: error: unsolved goals
beginEndAsMacro.lean:19:2: error: unsolved goals
x : Nat
⊢ x + 0 = x