Home |
Source |
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.
(* Simple usage *)
repeat split.
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