【发布时间】：2017-04-02 21:23:55
【问题描述】：
SF书中提到了以下文字：
这就是我们用 not 来表示 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
其实看着standard library，我 似乎找不到任何符号。那么，什么才是正确的 它的符号？
【问题讨论】：
-
不熟悉Coq类型语言，但是看标准库，肯定不等于应该是
<>或者<->？ -
@JonathonOgden 是的，你是对的。这是
<>。我看了看，但忽略了，因为它是对 monoid 的操作。 :) 你能把它作为答案发布吗？ -
完成。还建议查看@Elazar 答案。有道理。