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.