Stream: Coq users

Topic: overlapping notations in different scopes

Adrian Dapprich (Apr 05 2021 at 17:30):

Hi,
I was trying to use a notation involving a comma, which overlaps with the "forall A, B" syntax. It turns out that just declaring this notation without opening the containing scope already leads to an error which prevents me from using the forall syntax. I would have expected the error to only occur while the scope is open on the stack.
Maybe I'm understanding notation scopes wrong but this feels buggy.
This seems to apply to all notations that overlap in some way with others (e.g. also for "x | y" which overlaps with the dependent pairs) The notation for divisibility in Coq also uses braces so this seems like a known limitation.
So is the best way to wrap everything in braces in these cases?

Module inner_notations.

  Declare Scope myscope.

  Notation "x , y" := (plus x y) (at level 60) : myscope.
  Notation "x | y" := (plus x y) (at level 60) : myscope.

  (* #[ local ] *)
  (*  Open Scope myscope. *)
  (* Check 1 , 2. *)
  (* Check 1 | 2. *)
End inner_notations.

Import inner_notations.
Print Visibility.
Print Scopes.

(* Syntax error: '&' or '|' expected after [term level 200] (in [term]). *)
Definition bar : { n: nat | n = n }.
(* Syntax error: ',' expected after [open_binders] (in [binder_constr]). *)
Definition foo : forall _: nat, nat := fun x => x.

Paolo Giarrusso (Apr 05 2021 at 17:59):

It sounds like you’re interested in a newer feature called “custom entries”, which lets you add separate nonterminals to the grammar; by design, notation scopes don’t affect either the grammar or parsing at all — they only affect how the result of parsing is interpreted.

Paolo Giarrusso (Apr 05 2021 at 18:01):

FWIW, notations do respect Import at least — so even if you “load” a module which contains some notations, those will not be activated until the module is imported.

Adrian Dapprich (Apr 11 2021 at 00:57):

thanks Paolo I did not think about it that way. For the moment I've resortet to putting the notations into their own module so they don't interfere with the code until I need them.
When you say adding separate nonterminals, do you mean something like Expr in the docs (https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#custom-entries) is then considered a nonterminal? I always assumed that's already the behavior of normal notations but it seems then that custom notations are more appropriate to what I'm trying to do.

Paolo Giarrusso (Apr 11 2021 at 11:28):

Indeed: only custom entries create new nonterminals, not normal notations/scopes, but I agree this can be surprising.

Last updated: Sep 23 2023 at 08:01 UTC