Extra tactics and implementation for some tactics defined at Init/Tactic.lean

def Lean.Parser.Tactic.tacticIterate____ : ParserDescr

iterate n tac runs tac exactly n times. iterate tac runs tac repeatedly until failure.

iterate's argument is a tactic sequence, so multiple tactics can be run using iterate n (tac₁; tac₂; ⋯) or

iterate n
  tac₁
  tac₂
  ⋯

Equations

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

def Lean.Parser.Tactic.tacticRw_mod_cast___ : ParserDescr

Rewrites with the given rules, normalizing casts prior to each step.

Equations

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

def Lean.Parser.Tactic.tacticExact_mod_cast_ : ParserDescr

Normalize casts in the goal and the given expression, then close the goal with exact.

Equations

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

def Lean.Parser.Tactic.tacticApply_mod_cast_ : ParserDescr

Normalize casts in the goal and the given expression, then apply the expression to the goal.

Equations

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