Documentation

def Lean.Elab.runTactic (mvarId : Lean.MVarId) (tacticCode : Lean.Syntax) (ctx : optParam Lean.Elab.Term.Context Lean.Elab.runTactic.defaultContext) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := [], mvarErrorInfos := ∅, messages := { msgs := { 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 } }, letRecsToLift := [], infoState := { enabled := false, 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 } } }) :