Coq 中的 Unicode "not equal" 表示法 (≠)

Question

SF书中提到了以下文字：

这就是我们如何使用 not 声明 0 和 1 是 nat 的不同元素:

Theorem zero_not_one : ~(0 = 1).
Proof.
  intros contra. inversion contra.
Qed.
Such inequality statements are frequent enough to warrant a special notation, x ≠ y:
Check (0 ≠ 1).
(* ===> Prop *)

但是当我在 Coq 中实际这样做时：

Check (0 ≠ 1).

它给我这个错误：

Syntax Error: Lexer: Undefined token

事实上，查看标准图书馆, 我似乎找不到任何符号。那么，什么是合适的它的符号 ?

Answer 1

不熟悉 Coq 类型语言，但查看标准库，不等于 将写为 <>。

Answer 2

正如@jonathon所说，运算符写成<>.

Check 1 <> 2.

但你也可以这样做：

Require Import Unicode.Utf8.
Check 1 ≠ 2.

Coq 中的 Unicode "not equal" 表示法 (≠)

Unicode "not equal" notation in Coq (≠)

unicode

coq