coq: Eine linksrekursive Schreibweise muss eine explizite Ebene haben

Question

Ich habe eine Coq Notation Definition gesehen für „ausgewertet“ wie folgt:

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

Ich versuche, das Symbol '||' auf etwas anderes als || zu ändern wird oft für logische or verwendet. Allerdings habe ich immer einen Fehler

A left-recursive notation must have an explicit level 

Zum Beispiel geschieht dies, wenn ich '||' zu ändern:

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

Gibt es etwas Besonderes über || hier? und wie sollte ich es beheben, damit diese anderen Notationen funktionieren (wenn möglich)?

Answer 1

Wenn ich richtig bin, wenn Sie eine Notation überladen, verwendet Coq die Eigenschaften der ersten Definition. Die Notation _ '||' _ hat bereits eine Ebene, daher verwendet Coq diese Ebene für Ihre Definition.

Aber mit neuen Symbolen, Coq das nicht tun können, und Sie haben die Ebene zu spezifizieren:

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

Für bereits Notationen definiert, ist dies sogar stärker als das, was ich oben geschrieben habe. Sie können das Niveau einer Notation nicht neu definieren. Versuchen Sie zum Beispiel:

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