有一种方法可以禁用Coq中的特定符号？ 我希望在Coqide中拥有证据状态不使用某个符号（但仍然使用所有符号）。 这可能吗？

Question

这里描述了可能足够的一些技巧：

如何禁用我的Coq中的自定义符号？

我想添加指针以添加该答案，因为这个问题首先出现在Google上。

Answer 1

禁用

all

表示法，请使用

Answer 2

。但是，要禁用

特定符号，您可以使用Disable Notation和

Enable Notation

：

：

Answer 3

Disable Notation "+" (all).
    The following notations have been disabled:
    Notation "{ A } + { B }" := (sumbool A B) : type_scope
    Notation "A + { B }" := (sumor A B) : type_scope
    Notation "x + y" := (sum x y) : type_scope
    Notation "x + y" := (Nat.add x y) : nat_scope
    Notation "n + m" := (plus n m)
Enable Notation "_ + _" (all) : type_scope.
    The following notations have been enabled:
    Notation "x + y" := (sum x y) : type_scope
Disable Notation "x + y" := (sum x y).
    The following notations have been disabled:
    Notation "x + y" := (sum x y) : type_scope

从Https：//rocq-prover.org/doc/v8.18.0/refman/refman/user-extensions/syntax-extensions.html#enabling-and-disabling-notations-