def Lean.Elab.Tactic.evalWithAnnotateState : Tactic

def Lean.Elab.Tactic.evalDone : Tactic

def Lean.Elab.Tactic.evalSepTactics : Tactic

Evaluates a tactic script in form of a syntax node with alternating tactics and separators as children.

partial def Lean.Elab.Tactic.evalSepTactics.goEven (stx : Syntax) : TacticM Unit

partial def Lean.Elab.Tactic.evalSepTactics.goOdd (stx : Syntax) : TacticM Unit

def Lean.Elab.Tactic.evalSeq1 : Tactic

def Lean.Elab.Tactic.evalParen : Tactic

def Lean.Elab.Tactic.evalTacticSeq1Indented : Tactic

def Lean.Elab.Tactic.evalTacticSeqBracketed : Tactic

def Lean.Elab.Tactic.evalTacticCDot : Tactic

def Lean.Elab.Tactic.evalFocus : Tactic

def Lean.Elab.Tactic.evalRotateLeft : Tactic

def Lean.Elab.Tactic.evalRotateRight : Tactic

def Lean.Elab.Tactic.evalOpen : Tactic

def Lean.Elab.Tactic.elabSetOption : Tactic

def Lean.Elab.Tactic.evalAllGoals : Tactic

def Lean.Elab.Tactic.evalAnyGoals : Tactic

def Lean.Elab.Tactic.evalTacticSeq : Tactic

partial def Lean.Elab.Tactic.evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit

def Lean.Elab.Tactic.evalChoice : Tactic

def Lean.Elab.Tactic.evalSkip : Tactic

def Lean.Elab.Tactic.evalUnknown : Tactic

def Lean.Elab.Tactic.evalFailIfSuccess : Tactic

def Lean.Elab.Tactic.evalTraceState : Tactic

def Lean.Elab.Tactic.evalTraceMessage : Tactic

def Lean.Elab.Tactic.evalAssumption : Tactic

def Lean.Elab.Tactic.evalContradiction : Tactic

def Lean.Elab.Tactic.evalRefl : Tactic

def Lean.Elab.Tactic.evalIntro : Tactic

def Lean.Elab.Tactic.evalIntro.introStep (ref? : Option Syntax) (n : Name) (typeStx? : Option Syntax := none) : TacticM Unit

def Lean.Elab.Tactic.evalIntroMatch : Tactic

def Lean.Elab.Tactic.evalIntros : Tactic

def Lean.Elab.Tactic.evalRevert : Tactic

def Lean.Elab.Tactic.evalClear : Tactic

def Lean.Elab.Tactic.evalClearValue : Tactic

def Lean.Elab.Tactic.forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit

def Lean.Elab.Tactic.evalSubst : Tactic

def Lean.Elab.Tactic.evalSubstVars : Tactic

def Lean.Elab.Tactic.evalSubstEqs : Tactic

def Lean.Elab.Tactic.renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray `Lean.binderIdent) : TacticM MVarId

def Lean.Elab.Tactic.evalCase : Tactic

def Lean.Elab.Tactic.evalCase' : Tactic

def Lean.Elab.Tactic.evalRenameInaccessibles : Tactic

def Lean.Elab.Tactic.evalFirst : Tactic

partial def Lean.Elab.Tactic.evalFirst.loop (tacs : Array Syntax) (i : Nat) : TacticM Unit

def Lean.Elab.Tactic.evalFail : Tactic

def Lean.Elab.Tactic.evalDbgTrace : Tactic

def Lean.Elab.Tactic.evalSleep : Tactic

def Lean.Elab.Tactic.evalLeft : Tactic

def Lean.Elab.Tactic.evalRight : Tactic

def Lean.Elab.Tactic.evalReplace : Tactic

def Lean.Elab.Tactic.evalRunTac : Tactic