有没有办法禁用Coq中的特定符号？ [英] Is there a way to disable a specific notation in Coq?

问题描述

在Coqide中，我希望证明状态不使用某种符号（但仍使用所有其他符号）。

I'd like, in Coqide, to have the proof state not use a certain notation (but still use all others).

这可能吗？

推荐答案

根据我在文档中所了解的，这是不可能的。您也许可以使用打开/关闭范围，但是我不确定它是否会起作用，因为明确指出将在可能的情况下使用符号来进行打印。

From what I understand in the documentation, it is not possible. You might be able to play with opening/closing scopes but I'm not sure it will work, since it is stated explicitly that notations will be used for printing whenever possible.

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