test: for issue 2558

Issue has been fixed by another PR. closes #2558
2026-03-17 18:34:06 +00:00 · 2024-05-10 17:27:24 -07:00
1 changed files with 3 additions and 0 deletions
--- a/tests/lean/run/2558.lean
+++ b/tests/lean/run/2558.lean
@@ -0,0 +1,3 @@
+def even2 : sorry :=
+  have e : 1 + 1 = 2 := Eq.refl _
+  sorry