I'm planning to demonstrate Coq tactics to some graduate students studying type theory, and recently it seemed that many of the tactics could be re-defined with refine
: (feedback welcome) https://gist.github.com/siraben/d66cc482a5f38d8f80430932e62f7957
However, how would I implement someting like generalize dependent
using Ltac + refine?
All tactics boil down to refine. generalize dependent x
should be refine (_ H1 .. Hn x)
where H1 .. Hn
are the hypothesis in which x
occurs.
@Enrico Tassi do you need to clear H1 ... Hn
too?
Yes, and also x
Last updated: Oct 13 2024 at 01:02 UTC