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
@Enrico Tassi do you need to clear
H1 ... Hn too?
Yes, and also
Last updated: Oct 05 2023 at 02:01 UTC