Home |
Github |
The do tactical accepts a tactic t and a natural number n, applying t to the goal n times. do fails if one of the applications of t fails before n applications have occurred.
In my opinion, do is a difficult tactic to justify. I find myself using it when using repeat tends to be overzealous. For example, if I have a goal with 100 subterms, and I’d like to apply a tactic t only to 30 of the subterms (assuming t works on individual subterms and not the whole goal), I’m more likely to use do 30 t than repeat t to prevent the remaining 70 subterms from being affected.
do 3 (split; [reflexivity | idtac]).Before
=========================
1/1
1 = 1 /\ 2 = 2 /\ 3 = 3 /\ 4 = 4do 3 (split; [reflexivity | idtac]).After
No more goals.