Stream: Coq users

Topic: term sequences in ltac


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 06 2020 at 10:00):

In any case you don't have a first-class access to those sequences.

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Aug 06 2020 at 10:36):

Which is arguably also a hack.

view this post on Zulip Paolo Giarrusso (Aug 06 2020 at 20:32):

Wasn't this "fixed" in ltac2, at least since ltac2 has first class lists?

view this post on Zulip Paolo Giarrusso (Aug 06 2020 at 20:35):

(not sure about nice notations for it, but I'd be happy enough with lists)

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC