coq - Coq：未打印符号

Question

我定义了一个归纳类型，下面是最小的例子。我想使用符号，如 ~ 或 =。语法被识别，但未打印在右上角面板的目标中。

例子：

Inductive num : Set :=
  | O : num
  | S : num -> num.

Theorem test (n : num) : ~ (S n) = O.

小组说：

1 subgoal
n : num
______________________________________(1/1)
not (@eq num (S n) O)

虽然我期望：

1 subgoal
n : num
______________________________________(1/1)
~ (S n) = O

我试图重新定义 = 像这样，但没有成功：

Notation "x = y" := (@eq num x y) (at level 70).

或定义一个新符号，但均未成功：

Notation "x =n y" := (@eq num x y) (at level 50).
Theorem test (n : num) : ~ (S n) =n O.

是设置问题吗？我在 Mac 上使用 CoqIde 8.7.2。