coq: Una notazione sinistra-recursive deve avere un livello esplicito

Question

ho visto una definizione di notazione Coq per "restituisce" come segue:

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

Sto cercando di cambiare il simbolo '||' a qualcos'altro come || è spesso usato per il logico or. Tuttavia, ho sempre arrivare un errore

A left-recursive notation must have an explicit level 

Ad esempio, questo accade quando cambio '||' a:

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

C'è qualcosa di speciale su || qui? e come dovrei sistemarlo per far funzionare queste altre notazioni (se possibile)?

Answer 1

Se ho ragione, se sovraccarichi una notazione, Coq utilizza le proprietà della prima definizione. La notazione _ '||' _ ha già un livello, quindi Coq utilizza questo livello per la tua definizione.

Ma con nuovi simboli, Coq non può farlo, ed è necessario specificare il livello:

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

per iscrizioni già definiti, questo è ancora più forte di quello che ho scritto sopra. Non è possibile ridefinire il livello di una notazione. Prova ad esempio:

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