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