2d38a70d1c
This PR fixes a bug in `sym =>` interactive mode where satellite solvers (`lia`, `ring`, `linarith`) would throw an internal error if their automatic `intros + assertAll` preprocessing step already closed the goal. Previously, `evalCheck` used `liftAction` which discarded the closure result, so the subsequent `liftGoalM` call failed due to the absence of a main goal. `liftAction` is now split so the caller can distinguish the closed and subgoals cases and skip the solver body when preprocessing already finished the job. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
16 lines
402 B
Text
16 lines
402 B
Text
|
|
example (p q : Prop) : p → q → p ∧ q := by
|
|
sym =>
|
|
intro hp hq
|
|
apply And.intro
|
|
apply hp
|
|
apply hq
|
|
|
|
register_sym_simp chainSimp where
|
|
post := ground >> rewrite [Nat.add_zero, Nat.zero_add]
|
|
|
|
example (x y : Nat) (h : x ≤ y) : (1 - 1) + x ≤ y + (1 + 0) := by
|
|
sym =>
|
|
simp chainSimp
|
|
-- In the following tactic the goal is closed while preprocessing the target
|
|
lia
|