Stream: Coq users

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

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?

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.

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.

Ignat Insarov (Oct 02 2021 at 09:43):

I see.

Ignat Insarov (Oct 02 2021 at 09:43):

Thanks.

Notification Bot (Oct 02 2021 at 09:43):

Ignat Insarov has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC