Ali Caglayan (Aug 06 2020 at 00:03): Ali Caglayan (Aug 06 2020 at 00:03):Can term sequences such as the ones we can supply to apply or rewrite be used in ltac? For example, writing mytac t1, t2, t3 would essentially be shorthand for mytac t1; mytac t2; mytac t3.
Pierre-Marie Pédrot (Aug 06 2020 at 09:59):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.
Pierre-Marie Pédrot (Aug 06 2020 at 10:00):In any case you don't have a first-class access to those sequences.
Théo Winterhalter (Aug 06 2020 at 10:36):Besides the hack, there is also the option of definition tactic notations for each number of argument you want.
Théo Winterhalter (Aug 06 2020 at 10:36):Which is arguably also a hack.
Paolo Giarrusso (Aug 06 2020 at 20:32):Wasn't this "fixed" in ltac2, at least since ltac2 has first class lists?
Paolo Giarrusso (Aug 06 2020 at 20:35):(not sure about nice notations for it, but I'd be happy enough with lists)
Pierre-Marie Pédrot (Aug 06 2020 at 20:54):Yes, there are both a list datatype and a list scope for notations in Ltac2.
Last updated: Oct 03 2023 at 19:01 UTC