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 Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, autoBoundImplicitForbidden := fun (x : Lake.Name) => false, sectionVars := , sectionFVars := , implicitLambda := true, heedElabAsElim := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none, tacSnap? := none, saveRecAppSyntax := true, holesAsSyntheticOpaque := false }) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := , pendingMVars := , mvarErrorInfos := [], levelMVarErrorInfos := [], mvarArgNames := , letRecsToLift := [] }) :

Apply the give tactic code to mvarId in MetaM.

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