COQ：左遞歸符號必須有一個明確的級別

Question

我已經看到了Coq的符號定義「的計算結果爲」如下：

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

我想符號'||'更改爲別的東西作爲||經常被用於邏輯or。

'\|/'，'\||/'，'|_|'，'|.|'，'|v|'，或'|_'：不過，我總是得到一個錯誤

A left-recursive notation must have an explicit level 

例如，當我改變'||'到這種情況。

||這裏有什麼特別的嗎？我應該如何解決它以使這些其他符號有效（如果可能的話）？

Answer 1

如果我是對的，如果你重載一個符號，Coq使用第一個定義的屬性。記號_ '||' _已經有了一個級別，所以Coq使用這個級別來定義。

但隨着新的符號，勒柯克不能做到這一點，你必須指定的級別：

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

對於已經定義的符號，這是比我上面寫的更加強大。您無法重新定義符號的級別。試試例如：

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