5d54b0b13f
This PR fixes a bug introduced in #7830 where if the cursor is at the indicated position ```lean example (as bs : List Nat) : (as.append bs).length = as.length + bs.length := by induction as with | nil => -- cursor | cons b bs ih => ``` then the Infoview would show "no goals" rather than the `nil` goal. The PR also fixes a separate bug where placing the cursor on the next line after the `induction`/`cases` tactics like in ```lean induction as with | nil => sorry | cons b bs ih => sorry I -- < cursor ``` would report the original goal in the goal list. Furthermore, there are numerous improvements to error recovery (including `allGoals`-type logic for pre-tactics) and the visible tactic states when there are errors. Adds `Tactic.throwOrLogErrorAt`/`Tactic.throwOrLogError` for throwing or logging errors depending on the recovery state.
32 lines
1.4 KiB
Text
32 lines
1.4 KiB
Text
inductionErrors.lean:11:12-11:27: error: unsolved goals
|
|
case lower.h
|
|
p d : Nat
|
|
⊢ p ≤ p + d.succ
|
|
inductionErrors.lean:12:12-12:27: error: unsolved goals
|
|
case upper.h
|
|
q d : Nat
|
|
⊢ q + d.succ > q
|
|
inductionErrors.lean:16:19-16:26: error(lean.unknownIdentifier): Unknown identifier `elimEx2`
|
|
inductionErrors.lean:22:2-25:45: error: insufficient number of targets for 'elimEx'
|
|
inductionErrors.lean:28:16-28:23: error: expected resulting type of eliminator to be an application of one of its parameters (the motive):
|
|
Nat
|
|
inductionErrors.lean:35:11-35:15: error: unsolved goals
|
|
x : Nat
|
|
⊢ 0 + 0 = 0
|
|
inductionErrors.lean:36:11-36:15: error: unsolved goals
|
|
x y : Nat
|
|
⊢ 0 + (y + 1) = y + 1
|
|
inductionErrors.lean:40:14-40:18: error: unsolved goals
|
|
case zero
|
|
⊢ 0 + 0 = 0
|
|
inductionErrors.lean:41:14-41:18: error: unsolved goals
|
|
case succ
|
|
y : Nat
|
|
⊢ 0 + (y + 1) = y + 1
|
|
inductionErrors.lean:50:2-50:16: error: Alternative 'cons' is not needed
|
|
inductionErrors.lean:55:2-55:16: error: Alternative 'cons' is not needed
|
|
inductionErrors.lean:60:2-60:40: error: Invalid alternative name 'upper2': Expected 'upper'
|
|
inductionErrors.lean:58:2-58:7: error: Alternative 'upper' has not been provided
|
|
inductionErrors.lean:66:2-66:28: error: Invalid occurrence of the wildcard alternative `| _ => ...`: It must be the last alternative
|
|
inductionErrors.lean:74:2-74:34: error: Wildcard alternative is not needed
|
|
inductionErrors.lean:80:2-80:56: error: Duplicate alternative name 'lower'
|