def Lean.Elab.Tactic.evalWithAnnotateState : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalDone : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalSeq1 : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalParen : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.isCheckpointableTactic (arg : Lean.Syntax) : Lean.Elab.Tactic.TacticM Bool

def Lean.Elab.Tactic.addCheckpoints (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Lean.Syntax

Takes a sepByIndent tactic "; ", and inserts checkpoint blocks for save tactics.

Input:

  a
  b
  save
  c
  d
  save
  e

Output:

  checkpoint
    a
    b
    save
  checkpoint
    c
    d
    save
  e

def Lean.Elab.Tactic.evalSepByIndentTactic (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

Evaluate `sepByIndent tactic "; "

def Lean.Elab.Tactic.evalTacticSeq1Indented : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalTacticSeqBracketed : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalTacticCDot : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalFocus : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalRotateLeft : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalRotateRight : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalOpen : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.elabSetOption : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalAllGoals : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalAnyGoals : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalTacticSeq : Lean.Elab.Tactic.Tactic

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

def Lean.Elab.Tactic.evalChoice : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalSkip : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalUnknown : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalFailIfSuccess : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalTraceState : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalTraceMessage : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalAssumption : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalContradiction : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalRefl : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalIntro : Lean.Elab.Tactic.Tactic

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

def Lean.Elab.Tactic.evalIntroMatch : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalIntros : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalRevert : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalClear : Lean.Elab.Tactic.Tactic

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

def Lean.Elab.Tactic.evalSubst : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalSubstVars : Lean.Elab.Tactic.Tactic

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

def Lean.Elab.Tactic.evalCase : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalCase' : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalRenameInaccessibles : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalFirst : Lean.Elab.Tactic.Tactic

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

def Lean.Elab.Tactic.evalFail : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalDbgTrace : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.evalSleep : Lean.Elab.Tactic.Tactic