我定义了一个符号来模拟命令式编程
Notation "a >> b" := (b a) (at level 50).
然而之后，所有函数应用表达式都表示为“>>”样式。例如，在 Coq Toplevel 的证明模式下，我可以看到
bs' : nat >> list
而实际上应该是
bs' : list nat
为什么 Coq 积极地将所有函数应用程序风格的表达式重写为我定制的“>>”表示形式？我怎样才能将一切恢复正常，我的意思是我希望看到 'a >> b' 被解释为 'b a' 并且 'list nat' 不会被表示为 'nat >> list'？
谢谢你！
默认情况下，Coq 假设如果您定义了一个表示法，您希望它能够进行漂亮的打印。如果您希望符号永远不会出现在漂亮打印中，请将其声明为“仅解析”。
Notation "a >> b" := (b a) (at level 50, only parsing).
如果你想a >> b有时要显示，您可以将其限制在一个范围内，并将一个类型与该范围关联起来；那么只有当结果类型是该类型时才会应用符号。
没有办法告诉 Coq“仅在我在源代码中使用该符号的地方使用该符号”，因为用符号编写的术语与以任何其他方式编写的术语完全相同：最初使用的符号不是该符号的一部分。学期。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
