ink

def Lean.Elab.Tactic.evalTacticAtRaw (tac : Lean.Syntax) (mvarId : Lean.MVarId) : Lean.Elab.Tactic.TacticM (List Lean.MVarId)

Like evalTacticAt, but without restoring the goal list or pruning solved goals. Useful when these tasks are already being done in an outer loop.

Equations

• Lean.Elab.Tactic.evalTacticAtRaw tac mvarId = do Lean.Elab.Tactic.setGoals [mvarId] Lean.Elab.Tactic.evalTactic tac Lean.Elab.Tactic.getGoals