如何解决为嵌入式逻辑定义自定义符号时出错
我正在将模态逻辑嵌入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手册也不是很有帮助。
是什么原因导致此错误,以及其他标记为何起作用?
解决方法
您为逻辑声明了自己的语法类别:解析器在[!
之后,仅期望条目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 !] .
我在SO上发现了一些问题,建议的解决方案是更改第一个符号(在这种情况下为p)的优先级,但这只会引发另一个错误。 Coq手册也不是很有帮助。
如果您的符号最左边的符号是一个终端而不是一个变量,这可能是一个解决方案。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。