Coq中的Unicode"不等于"表示法(≠)

Question

SF书中提到了以下文字:

这就是我们如何使用不表示0和1是nat的不同元素:

Theorem zero_not_one : ~(0 = 1).
Proof.
  intros contra. inversion contra.
Qed.

这种不等式陈述经常足以保证特殊符号,x≠y:

Check (0 ? 1).
(* ===> Prop *)

但是当我在Coq中实际执行此操作时:

Check (0 ? 1).

它给了我这个错误:

Syntax Error: Lexer: Undefined token

事实上,看看标准库,我似乎找不到任何符号.那么,它的正确表示法是什么？

Answer 1

正如@jonathon所说,运营商是写的<>.

Check 1 <> 2.

但你也可以这样做:

Require Import Unicode.Utf8.
Check 1 ? 2.