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.
```

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.

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.

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.

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

Last updated: Jun 18 2024 at 23:01 UTC