如何在Coq中禁用我的自定义符号？ [英] How to disable my custom notation in Coq?

问题描述

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

I've defined a notation to simulate imperative style programming by

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

不过，此后，所有函数应用程序表达式都表示为 >>样式。例如，在Coq顶级的证明模式下，我可以看到

However after that, all function-application expression are represented as '>>' style. For example, in proof mode of Coq Toplevel, I can see

bs' : nat >> list

而实际上应该是

bs' : list nat

为什么积极地使用Coq将所有功能应用程序样式的表达式重写为我的自定义 >>表示形式？如何将所有内容恢复为正常状态，我想将 a >> b解释为 b a和 list nat将不会表示为 nat >>列表吗？

Why does Coq aggressively rewrite all function application styled expression into my customized '>>' representation? How can I restore everything back to normal, I mean I want to see 'a >> b' be interpreted as 'b a' and 'list nat' will not be represented as 'nat >> list'?

谢谢！

推荐答案

默认情况下，Coq假定如果您定义了一种表示法，则希望将其用于漂亮的打印。如果您希望该符号永远不会出现在漂亮的打印中，则将其声明为仅解析。

By default, Coq assumes that if you define a notation, you want to it for pretty-printing. If you want the notation to never appear in pretty-printing, declare it as "only parsing".

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

如果要 a>> b 有时会显示出来，您可以将其限制在一个范围内，并将类型关联到该范围；

If you want a >> b to be displayed sometimes, you can restrict it to a scope and associate a type to this scope; then the notation will only be applied when the result type is that type.

没有办法告诉Coq仅在源代码中使用该符号的地方使用 ，因为用符号书写的术语与以任何其他方式书写的术语完全相同：最初使用的符号不是该术语的一部分。

There's no way to tell Coq "use the notation only where I used it in my source code", because a term written with a notation is exactly the same as the term written in any other way: the notation used originally is not part of the term.

这篇关于如何在Coq中禁用我的自定义符号？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！