Additions to Lean.Elab.Tactic.Meta

def Lean.Elab.runTactic' (mvarId : MVarId) (tacticCode : Syntax) (ctx : Term.Context := { }) (s : Term.State := { }) : MetaM (List MVarId)

Apply the given tactic code to mvarId in MetaM.

This is a variant of Lean.Elab.runTactic that forgets the final Term.State.

Equations

• One or more equations did not get rendered due to their size.