repeat

The repeat tactical repeatedly executes a tactic until it either fails or causes no change in the goal. If the tactic provided succeeds, it will be recursively applied to each generated subgoal.

Syntax

(* Simple usage *)
repeat split.

Examples

Before

P, Q, R, S: Prop
-------------------------
1/1
P /\ Q /\ R /\ S

repeat split.

After

P, Q, R, S: Prop
-------------------------
1/4
P
-------------------------
2/4
Q
-------------------------
3/4
R
-------------------------
4/4
S

Resources

Reference Documentation

---