如何在Coq中禁用我的自定义表示法？

Question

我已经定义了一个符号来模拟命令式样式编程

Notation "a >> b" := (b a) (at level 50).

然而,之后,所有函数应用程序表达式都表示为">>"样式.例如,在Coq Toplevel的证明模式中,我可以看到

bs' : nat >> list

实际上它应该是

bs' : list nat

为什么Coq积极地将所有函数应用程序样式表达式重写为我的自定义">>"表示？如何将一切恢复正常,我的意思是我想看到'a >> b'被解释为'ba'而'list nat'将不会被表示为'nat >> list'？

谢谢!

Answer 1

默认情况下,Coq假定如果您定义表示法,则需要将其用于漂亮打印.如果您希望符号永远不会出现在漂亮的打印中,请将其声明为"仅解析".

Notation "a >> b" := (b a) (at level 50, only parsing).

如果您希望a >> b有时显示,可以将其限制为范围并将类型与此范围关联; 然后只有在结果类型是该类型时才会应用表示法.

没有办法告诉Coq"只使用我在源代码中使用它的符号",因为用符号写的术语与用其他任何方式编写的术语完全相同:最初使用的符号不是术语.

Answer 2

您可以使用定义.这样,只有标记为"followBy"的内容才会以这种方式显示.否则,机器无法知道何时使用空格而不是">>"......

Definition followedBy {A B : Type} (a : A) (b : A -> B) := b a.

Notation "a >> b" := (followedBy a b) (at level 50).