CODEWITHSUNDEEP
coqnotation
thor
thor

Reputation: 22500

coq: A left-recursive notation must have an explicit level

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

 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)?

Upvotes: 6

Views: 1078

Answers (1)

eponier
eponier

Reputation: 3122

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.

Upvotes: 5

Related Questions