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
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.
if you care, examples include
…/ltac_tactics.v in iris. Let me know if I should hunt down a link.
Ignat Insarov has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC