coq：左递归符号必须有一个明确的级别答案

【问题标题】：coq: A left-recursive notation must have an explicit levelcoq：左递归符号必须有一个明确的级别
【发布时间】：2015-11-26 01:35:17
【问题描述】：

我看到了一个 Coq 符号定义“评估到”如下：

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

我正在尝试将符号 '||' 更改为其他符号，因为 || 经常用于逻辑 or。但是，我总是收到错误

 A left-recursive notation must have an explicit level

例如，当我将'||' 更改为：

'\|/'、'\||/'、'|_|'、'|.|'、'|v|' 或 '|_'。

|| 这里有什么特别之处吗？以及我应该如何修复它以使这些其他符号工作（如果可能的话）？

【问题讨论】：

【解决方案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.

【讨论】：