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

事实上，看看 standardlibrary ， 我似乎找不到任何符号。那么，什么才是正确的它的符号？

Answer 1

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

Check 1 <> 2.

但你也可以这样做:

Require Import Unicode.Utf8.
Check 1 ≠ 2.