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.