def
Lean.Elab.runTactic
(mvarId : MVarId)
(tacticCode : Syntax)
(ctx : Term.Context :=
{ declName? := none, auxDeclToFullName := ∅, macroStack := [], mayPostpone := true, errToSorry := true,
autoBoundImplicit := false,
autoBoundImplicits :=
{ root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat),
tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift,
tailOff := 0 },
autoBoundImplicitForbidden := fun (x : Name) => false, sectionVars := ∅, sectionFVars := ∅, implicitLambda := true,
heedElabAsElim := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false,
tacticCache? := none, tacSnap? := none, saveRecAppSyntax := true, holesAsSyntheticOpaque := false,
checkDeprecated := true })
(s : 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.