Documentation

Lean.Elab.Tactic.Meta

def Lean.Elab.runTactic (mvarId : Lean.MVarId) (tacticCode : Lean.Syntax) (ctx : optParam Lean.Elab.Term.Context { declName? := none, auxDeclToFullName := , macroStack := [], mayPostpone := true, errToSorry := true, autoBoundImplicit := false, autoBoundImplicits := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, autoBoundImplicitForbidden := fun x => false, sectionVars := , sectionFVars := , implicitLambda := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none, saveRecAppSyntax := true, holesAsSyntheticOpaque := false }) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := , pendingMVars := , mvarErrorInfos := , letRecsToLift := [] }) :

Apply the give tactic code to mvarId in MetaM.

Instances For