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?
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.
The good news is that you can probably do that directly using Ltac2 notations.
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: Oct 03 2023 at 20:01 UTC