From d4eed2e4903a3fb5389da97f30e2ab47677fa56e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jun 2022 15:40:13 -0700 Subject: [PATCH] test: test for #1267 --- tests/lean/run/1267.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 tests/lean/run/1267.lean diff --git a/tests/lean/run/1267.lean b/tests/lean/run/1267.lean new file mode 100644 index 0000000000..2f0730174e --- /dev/null +++ b/tests/lean/run/1267.lean @@ -0,0 +1,13 @@ +example : 1 = 2 := calc + _ = _ := sorry + +example : 1 = 2 := + calc + _ = _ := sorry + +example : 1 = 2 := by calc + _ = _ := sorry + +example : 1 = 2 := by + calc + _ = _ := sorry