Coq: left recursive designation must have an explicit level

Question

I saw the definition of the Coq notation for “evaluated” as follows:

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

I am trying to change the character '||' to something else since || often used for logical or . However, I always get an error message

  A left-recursive notation must have an explicit level 

For example, this happens when I change '||' on the:

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

Is there anything special in || here? and how can I fix it to make these other notations (if possible)?

Answer 1

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

But with new characters, Coq cannot do this, and you must specify the level:

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

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

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