有没有办法在Coq中禁用特定的符号？

Question

在Coqide中,我希望证明状态不使用某种符号(但仍然使用所有其他符号).

这可能吗？

Answer 1

据我在文档中的理解，这是不可能的。您也许可以使用打开/关闭范围，但我不确定它是否有效，因为明确指出符号将尽可能用于打印。