Ben Siraphob (May 16 2021 at 12:58): Ben Siraphob (May 16 2021 at 12:58):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?
Enrico Tassi (May 16 2021 at 13:07):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.
Emilio Jesús Gallego Arias (May 16 2021 at 13:35):@Enrico Tassi do you need to clear H1 ... Hn too?
Enrico Tassi (May 16 2021 at 13:41):Yes, and also x
Last updated: Oct 13 2024 at 01:02 UTC