Skip to content

Commit 5588839

Browse files
committed
improve test
1 parent b8f47e8 commit 5588839

File tree

1 file changed

+6
-3
lines changed

1 file changed

+6
-3
lines changed

tests/lean/run/showTactic.lean

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -78,20 +78,23 @@ example : x = 0 ∧ x = 1 ∧ x = 2 ∧ x = 3 := by
7878
show _ = 2
7979

8080
/-!
81-
The goals before the last one are elaborated without error recovery.
81+
All goals except the first one are elaborated without error recovery.
8282
-/
8383

8484
/--
8585
error: unsolved goals
86-
case refine_2
86+
case refine_2.refine_2
8787
a : Unit
8888
⊢ a = ()
8989
9090
case refine_1
9191
⊢ () = ()
92+
93+
case refine_2.refine_1
94+
⊢ () = ()
9295
-/
9396
#guard_msgs in
94-
example : () = () ∧ (∀ a, a = ()) := by
97+
example : () = () ∧ () = () ∧ (∀ a, a = ()) := by
9598
and_intros; all_goals try intro a
9699
show a = _
97100

0 commit comments

Comments
 (0)