Stream: Coq users

Topic: ✔ How to write tactics that accept any number of parameters?


view this post on Zulip Ignat Insarov (Oct 01 2021 at 10:06):

For example, consider this trivial definition:

Ltac suppose := intros.

suppose will not accept any arguments, even though intros does. How can I generalize suppose to behave exactly like intros?

view this post on Zulip Paolo Giarrusso (Oct 01 2021 at 21:54):

I don’t think you could write anything close to intros in Ltac1. You can sort-of write “variadic tactics”, but painfully — decide the maximum number of arguments n you want to support (say, 5, 10, ….), and write n Tactic Notations.

view this post on Zulip Paolo Giarrusso (Oct 01 2021 at 21:55):

if you care, examples include …/ltac_tactics.v in iris. Let me know if I should hunt down a link.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 09:43):

I see.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 09:43):

Thanks.

view this post on Zulip Notification Bot (Oct 02 2021 at 09:43):

Ignat Insarov has marked this topic as resolved.


Last updated: Feb 04 2023 at 21:02 UTC