Documentation

Init.TacticsExtra

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

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
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For

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

              Equations
                Instances For