Julin S (Apr 20 2022 at 14:11): Julin S (Apr 20 2022 at 14:11):I was trying to have another interpretation for the [] notation, in addition to it meaning List.nil from ListNotations.
Require Import List.
Import ListNotations.
Module EgNotations.
Declare Scope eg_scope.
Delimit Scope eg_scope with eg.
Notation "[ ]" := 3
(at level 30) : eg_scope. (* No error if level is not set *)
(*
Notation "[ ]" is already defined at level 0 with arguments
while it is now required to be at level 30 with arguments .
*)
End EgNotations.
I had used a different notation scope named eg_scope for the 2nd interpretation, but it still gives error.
The manual says:
If a notation is defined in multiple scopes, Coq uses the interpretation from the most recently opened notation scope or declared lonely notation.
But in this case, the second notation hasn't even been defined yet.
Among other things, Print Visibility. gives:
Visible in scope list_scope
"x :: y" := cons x y
"x ++ y" := app x y
"[ x ]" := cons x nil
"[ x ; y ; .. ; z ]" := cons x (cons y .. (cons z nil) ..)
"[ ]" := nil
Any idea where I am going wrong?
Li-yao (Apr 20 2022 at 14:21):There can only ever be one level for a notation. And I'm not sure there's any point to setting a level for this notation anyway.
Li-yao (Apr 20 2022 at 14:21):The scope affects how the notation is interpreted only after precedence has been resolved.
Paolo Giarrusso (Apr 20 2022 at 14:39):I'll never find the time :-(, but I'd love to add to the manual the pipeline the parsing-interpretation pipeline that notations go through, and how notations are phase split between the "grammar part" visible in Reserved Notation (which affects parsing, but ignores the right-hand sides and scopes) and the "interpretations" (what's left after Reserved Notation).
Paolo Giarrusso (Apr 20 2022 at 14:41):@Julin S IOW, your notation splits into:
Reseved Notation "[ ]" (at level 30).
Notation "[ ]" := 3 : eg_scope.
Scopes don't exist in the first part, which is all the parser sees. And that's why what matters to the parser can't depend on scopes.
Paolo Giarrusso (Apr 20 2022 at 14:42):it probably doesn't matter for [], but since it might matter for your next notation: if you want different grammar rules, you probably need new nonterminals (or "custom entries" in camlp5/Coq's jargon)
Julin S (Apr 21 2022 at 04:32):Thanks. So notation levels are fixed. Only interpretations can differ.
Notification Bot (Apr 21 2022 at 04:32):Julin S has marked this topic as resolved.
Last updated: Oct 03 2023 at 04:02 UTC