Remy Seassau (Dec 04 2023 at 15:52): Remy Seassau (Dec 04 2023 at 15:52):Hello everyone,
I am trying to write a tactic which requires the use of pattern on multiple terms (e.g. pattern x, y, z in H).
I was struggling to handle lists of arguments using Ltac and was hoping that Ltac2's support for notations of the form
Ltac2 Notation "tac" arg(list1(constr, ",")) := ...
could be a good starting point for passing multiple arguments to pattern. However, I have been unable to make any progress from here and was wondering if such an approach is intended/viable.
Gaëtan Gilbert (Dec 04 2023 at 15:54):not sure what the problem is
what did you try and how did it fail?
Remy Seassau (Dec 04 2023 at 16:01):I was hoping to have something of the form
Ltac2 Notation "tac" arg(list1(constr, ",")) :=
...
pattern arg in H;
...
But haven't found a way to coerce arg : constr list to something that I can pass as an argument to pattern.
Last updated: Oct 12 2024 at 11:01 UTC