Can term sequences such as the ones we can supply to
rewrite be used in ltac? For example, writing
mytac t1, t2, t3 would essentially be shorthand for
mytac t1; mytac t2; mytac t3.
The answer is mostly no. You can hack around this by using tactic notations and hoping that the target tactic accepts treating lists of terms as terms, which is the case for all tactics defined through a TACTIC EXTEND with a constr argument. Outside of that fragment, this will fail badly.
In any case you don't have a first-class access to those sequences.
Besides the hack, there is also the option of definition tactic notations for each number of argument you want.
Which is arguably also a hack.
Wasn't this "fixed" in ltac2, at least since ltac2 has first class lists?
(not sure about nice notations for it, but I'd be happy enough with lists)
Yes, there are both a list datatype and a list scope for notations in Ltac2.
Last updated: Oct 03 2023 at 19:01 UTC