Stream: Coq users

Topic: Ltac2 array literals


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

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

view this post on Zulip Pierre-Marie Pédrot (Feb 02 2021 at 12:26):

The good news is that you can probably do that directly using Ltac2 notations.

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC