def
Lean.Elab.runTactic
(mvarId : Lean.MVarId)
(tacticCode : Lean.Syntax)
(ctx : optParam Lean.Elab.Term.Context
{ declName? := none, macroStack := [], mayPostpone := true, errToSorry := true, autoBoundImplicit := false,
autoBoundImplicits :=
{ root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)),
tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0,
shift := Std.PersistentArray.initShift, tailOff := 0 },
autoBoundImplicitForbidden := fun x => false, sectionVars := ∅, sectionFVars := ∅, implicitLambda := true,
isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none,
saveRecAppSyntax := true })
(s : optParam Lean.Elab.Term.State
{ levelNames := [], syntheticMVars := [], mvarErrorInfos := ∅, letRecsToLift := [],
infoState :=
{ enabled := true,
assignment :=
{ root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
trees :=
{ root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)),
tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0,
shift := Std.PersistentArray.initShift, tailOff := 0 } } })
:
Apply the give tactic code to mvarId in MetaM.
Equations
- One or more equations did not get rendered due to their size.