Lean4
/-- Copy of `Lean.Elab.Tactic.run` that can return a value. -/
-- We need this because Lean 4 core only provides `TacticM` functions for building simp contexts,
-- making it quite painful to call `simp` from `MetaM`.
def run_for (mvarId : MVarId) (x : TacticM α) : TermElabM (Option α × List MVarId) :=
mvarId.withContext do
let pendingMVarsSaved := (← get).pendingMVars
modify fun s => { s with pendingMVars := [] }
let aux : TacticM (Option α × List MVarId) :=
/- Important: the following `try` does not backtrack the state.
This is intentional because we don't want to backtrack the error message
when we catch the "abort internal exception"
We must define `run` here because we define `MonadExcept` instance for `TacticM` -/
try
let a ← x
pure (a, ← getUnsolvedGoals)
catch ex =>
if isAbortTacticException ex then
pure (none, ← getUnsolvedGoals)
else
throw ex
try
aux.runCore' { elaborator := .anonymous } { goals := [mvarId] }
finally
modify fun s => { s with pendingMVars := pendingMVarsSaved }
