为嵌入式逻辑定义自定义符号时出错

Question

我正在研究同事在 Coq 中嵌入模态逻辑的问题，我正在尝试为所述逻辑的公式定义自定义符号，如 here 以及软件一书第 2 卷中介绍的那样基金会。到目前为止我有这个：

Declare Custom Entry modal.
Declare Scope modal_scope.

Notation "[! m !]"    := m (at level 0, m custom modal at level 99) : modal_scope.
Notation " p -> q "   := (Implies p q) (in custom modal at level 13, right associativity).

Open Scope modal_scope.

Definition test:
  [! p -> q !].

然而，Definition 给出了这个错误：

Syntax error: [constr:modal level 99] expected after '[!' (in [constr:operconstr]).

而且我不明白为什么。我在 SO 上发现了一些问题，其中建议的解决方案是更改第一个符号的优先级，在这种情况下为 p，但这只会引发另一个错误。 Coq 手册也不是很有帮助。

导致此错误的原因是什么以及为什么其他符号有效？

Answer 1

您为自己的逻辑声明了自己的句法类别：[! 之后的解析器只需要条目 modal 中的内容。 p 是一个标识符，解析器不期望任意标识符。

在 documentation on custom entries 中，您可以找到有关如何将标识符添加到您的条目的提示：

Declare Custom Entry modal.
Declare Scope modal_scope.

Print Grammar constr.

Axiom Implies : Prop -> Prop -> Prop.

Notation "x" := x (in custom modal at level 0, x ident).

Notation "[! m !]"    := m (at level 0, m custom modal at level 99) : modal_scope.
Notation "p '->' q"   := (Implies p q) (in custom modal at level 13, right associativity).

Open Scope modal_scope.

Definition testp p q:
  [! p -> q !] .

I found some questions on SO where the suggested solution is to change the precedence of the first symbol, p in this case, however that just throws another error. The Coq manual wasn't very helpful either.

如果您的符号最左边的符号是终结符号而不是变量，这可能是一个解决方案。

为嵌入式逻辑定义自定义符号时出错

Error when defining custom notation for an embedded logic

coq

notation