# Documentation

Lean.Elab.Tactic.BuiltinTactic

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• = let kind := ; pure (kind == Lean.Parser.Tactic.save)

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

Equations
• One or more equations did not get rendered due to their size.

Evaluate sepByIndent tactic "; "

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Tactic.evalChoiceAux (tactics : ) (i : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.evalIntro.introStep (ref : ) (n : Lean.Name) (typeStx? : optParam () none) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
def Lean.Elab.Tactic.renameInaccessibles (mvarId : Lean.MVarId) (hs : Lean.TSyntaxArray `Lean.binderIdent) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Tactic.evalFirst.loop (tacs : ) (i : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations