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?

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.

The scope affects how the notation is interpreted only after precedence has been resolved.

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`

).

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

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)

Thanks. So notation levels are fixed. Only interpretations can differ.

Julin S has marked this topic as resolved.

Last updated: Jun 24 2024 at 00:02 UTC