本文介绍了有没有办法禁用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中的特定符号？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！