From 9d32d7bcf5eac4a044e07441ed8fb6550dc2c61f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Mar 2022 14:14:28 -0700 Subject: [PATCH] test: for issue #1062 closes #1062 --- tests/lean/1062.lean | 11 +++++++++++ tests/lean/1062.lean.expected.out | 1 + 2 files changed, 12 insertions(+) create mode 100644 tests/lean/1062.lean create mode 100644 tests/lean/1062.lean.expected.out diff --git a/tests/lean/1062.lean b/tests/lean/1062.lean new file mode 100644 index 0000000000..6b397ac9ee --- /dev/null +++ b/tests/lean/1062.lean @@ -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 diff --git a/tests/lean/1062.lean.expected.out b/tests/lean/1062.lean.expected.out new file mode 100644 index 0000000000..1ebc0b0b70 --- /dev/null +++ b/tests/lean/1062.lean.expected.out @@ -0,0 +1 @@ +1062.lean:11:2-11:7: error: no goals to be solved