为嵌入逻辑定义自定义表示法时出错

Question

我正在研究一位同事在Coq中嵌入模态逻辑的问题，我正试图为所述逻辑的公式定义一个自定义表示法，就像这里和《软件基础》一书的第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是一个标识符，解析器不期望有任意的标识符。

在关于自定义条目的文档中，您可以找到如何向条目添加标识符的提示：

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 !] .

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

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