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

test: for issue #1062

Browse source 
closes #1062
This commit is contained in:
Leonardo de Moura 2022-03-22 14:14:28 -07:00
parent 2f67140603
commit 9d32d7bcf5
2 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
tests/lean/1062.lean Normal file
View file

@ -0,0 +1,11 @@
example : if x = 0 then y + x = y else x ≠ 0 := by
simp (config := { contextual := true })
example : if x = 0 then y + x = y else x ≠ 0 := by
split
simp_all
simp_all
example : if x = 0 then y + x = y else x ≠ 0 := by
simp (config := { contextual := true })
split -- Error: no goals to be solved

1
tests/lean/1062.lean.expected.out Normal file
View file

@ -0,0 +1 @@
1062.lean:11:2-11:7: error: no goals to be solved