Janno (Feb 02 2021 at 08:38): Janno (Feb 02 2021 at 08:38):My Ltac2 code is full of array_of_list [a; b; c] and I have never liked that part very much. I was reading the documentation and saw this: "There is dedicated syntax for list and array literals." But I only see syntax for list literals in the grammar rules that follow this statement. So what's the story here? Can I write array literals?
Pierre-Marie Pédrot (Feb 02 2021 at 12:23):I think the documentation is wrong. IIRC I wrote it for an experimental branch that had the syntax but I had to remove it. The standard OCaml array notation is tricky in Ltac2 because it is incompatible with other parsing rules, so we should come up with a syntax mostly compatible with the rest of the parsing rules.
Pierre-Marie Pédrot (Feb 02 2021 at 12:26):The good news is that you can probably do that directly using Ltac2 notations.
Janno (Aug 27 2021 at 10:25):I have been playing around with this but I cannot find any symbol(s) to use such that the notation parses the same as list notations, i.e. without requiring extra parentheses around it. I think I am doing the same thing that is done in g_ltac2.mlg for lists:
#[global]
Ltac2 Notation "«" l(list0(tactic(5), ";")) "»" : 0 :=
array_of_list l.
Ltac2 Eval (fun x => x) (« 5; 7 »).
Fail Ltac2 Eval (fun x => x) « 5; 7 ».
The same result happens for any combination of brackets, parantheses, pipes, etc.. that I have tested
Last updated: Apr 20 2024 at 14:01 UTC