有沒有辦法在Coq中禁用特定的符號？

Question

我希望在Coqide中證明狀態不使用某種表示法（但仍使用其他表示法）。

這可能嗎？

Answer 1

根據我在文檔中的理解，這是不可能的。您可能可以使用打開/關閉範圍，但我不確定它會起作用，因爲它明確指出，只要有可能，將使用符號進行打印。

Answer 2

一些技巧，可能就足夠了描述如下：How to disable my custom notation in Coq?

我想指針到這個問題的答案，因爲這個問題來了第一個在谷歌。