Stream: Coq users

Topic: building tactics from `refine`


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2021 at 13:35):

@Enrico Tassi do you need to clear H1 ... Hn too?

view this post on Zulip Enrico Tassi (May 16 2021 at 13:41):

Yes, and also x


Last updated: Jan 27 2023 at 02:04 UTC