coq:左递归表示法必须具有显式级别

Question

我已经看到"评估为"的Coq符号定义如下:

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

我试图将符号更改为'||'其他符号,这||通常用于逻辑or.但是,我总是得到一个错误

 A left-recursive notation must have an explicit level

例如,当我'||'改为:

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

||这里有什么特别的东西吗？我应该如何修复它以使这些其他符号起作用(如果可能的话)？

Answer 1

如果我是对的,如果你重写符号,Coq使用第一个定义的属性.符号_ '||' _已经有一个级别,因此Coq使用此级别进行定义.

但是对于新的符号,Coq不能这样做,你必须指定级别:

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

对于已定义的符号,这甚至比我上面写的更强.您无法重新定义表示法的级别.试试例子:

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