Search code examples
coqcoq-tactic

How could we specify the times of running a tactic

I want to run a tactic several times. For instance, I want to execute apply lemma1 two times but do not like to write like apply lemma1. apply lemma1. Is there a command such that I can apply apply lemma1. for just two times?

Solution

  • do 2 apply lemma1.

    There is a whole page on tactic combinators and how to create new tactics: https://coq.inria.fr/refman/proof-engine/ltac.html#do-loop