Coq: a left-recursive notation must have an explicit level

Question

I have seen a Coq notation definition for "evaluates to" as follows:

Notation "e '||' n" := (aevalR e n) : type_scope.

I am trying to change the symbol '||' to something else as || is often times used for logical or. However, I always get an error

The command has indeed failed with message:
A left-recursive notation must have an explicit level.

For example, this happens when I change '||' to:

'\|/', '\||/', '|_|', '|.|', '|v|', or '|_'.

Is there something special about || here? and how should I fix it to make these other notations work (if possible)?

Answer

If I am right, if you overload a notation, Coq uses the properties of the first definition. The notation _ '||' _ has already a level, so Coq uses this level for your definition.

But with new symbols, Coq cannot do that, and you have to specify the level:

Notation "e '|.|' n" := (aevalR e n) (at level 50) : type_scope.

For already defined notations, this is even stronger than what I wrote above. You cannot redefine the level of a notation. Try for example:

Notation "e '||' n" := (aevalR e n) (at level 20) : type_scope.
Notation "_ || _" was already defined with a different
format. [notation-incompatible-format,parsing]
Notation "_ || _" is already defined at level 50
with arguments constr at level 50, constr
at next level while it is now required to be
at level 20 with arguments constr at next level,
constr at next level.