d9c3bbf1b4
This PR fixes an issue where the `induction` and `cases` tactics would swallow diagnostics (such as unsolved goals errors) when the `using` clause contains a nested tactic. Closes #12815
16 lines
467 B
Text
16 lines
467 B
Text
/-! Diagnostics from induction alternatives must not be swallowed when the `using`
|
|
clause contains a nested `by` tactic block. https://github.com/leanprover/lean4/issues/12815 -/
|
|
|
|
axiom myElim (h : True) (P : Nat → Prop) (n : Nat)
|
|
(zero : P 0) (succ : ∀ n, P n → P (n + 1)) : P n
|
|
|
|
/--
|
|
error: unsolved goals
|
|
case zero
|
|
⊢ True
|
|
-/
|
|
#guard_msgs in
|
|
theorem foo : True := by
|
|
induction 0 using myElim (by trivial) with
|
|
| zero => skip
|
|
| succ _ ih => exact ih
|