如何在 Coq 中禁用我的自定义符号？
How to disable my custom notation in Coq?
我已经通过
定义了一个符号来模拟命令式编程
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'?
谢谢！
您可以改用定义。这样，只有您标记为 "followedBy" 的内容才会以这种方式具体化。否则机器无法知道何时使用 space 与 ">>"...
Definition followedBy {A B : Type} (a : A) (b : A -> B) := b a.
Notation "a >> b" := (followedBy a b) (at level 50).
默认情况下，Coq 假设如果您定义了一个符号，您希望它用于漂亮的打印。如果您希望该符号永远不会出现在漂亮的打印中，请将其声明为“仅解析”。
Notation "a >> b" := (b a) (at level 50, only parsing).
如果你希望有时显示a >> b，你可以将它限制在一个范围内，并为这个范围关联一个类型；那么只有当结果类型是该类型时才会应用该符号。
没有办法告诉 Coq “仅在我在源代码中使用它的地方使用符号”，因为用符号编写的术语与以任何其他方式编写的术语完全相同：最初使用的符号不是术语的一部分。
我已经通过
定义了一个符号来模拟命令式编程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'?
谢谢！
您可以改用定义。这样，只有您标记为 "followedBy" 的内容才会以这种方式具体化。否则机器无法知道何时使用 space 与 ">>"...
Definition followedBy {A B : Type} (a : A) (b : A -> B) := b a.
Notation "a >> b" := (followedBy a b) (at level 50).
默认情况下，Coq 假设如果您定义了一个符号，您希望它用于漂亮的打印。如果您希望该符号永远不会出现在漂亮的打印中，请将其声明为“仅解析”。
Notation "a >> b" := (b a) (at level 50, only parsing).
如果你希望有时显示a >> b，你可以将它限制在一个范围内，并为这个范围关联一个类型；那么只有当结果类型是该类型时才会应用该符号。
没有办法告诉 Coq “仅在我在源代码中使用它的地方使用符号”，因为用符号编写的术语与以任何其他方式编写的术语完全相同：最初使用的符号不是术语的一部分。