的Unicode在Coq的（≠）“不等于”符号

这是我们如何使用并不表明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 *) 

但我真正做到这一点的勒柯克时：

它给我这个错误：

Syntax Error: Lexer: Undefined token

实际上，看着standard library，I 似乎无法找到任何符号。那么，适合的符号是什么呢？

来源

2017-04-02 Sibi

不熟悉勒柯克类型的语言，但是看一下标准库，想必_not等于to_是'<>'或''<->？ –

@JonathonOgden是的，你是对的。这是'<>'。我看着那个，但是被忽视，因为它是在monoids上操作的。 :)你可以张贴作为答案？ – Sibi

完成。还建议看到@Elazar答案。说得通。 –

正如@jonathon所说，操作员写的是<>。

Check 1 <> 2.

但是你也可以这样做：

Require Import Unicode.Utf8. 
Check 1 ≠ 2.

来源

2017-04-02 21:46:33 Elazar

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

来源

2017-04-02 21:42:42

'<->'是“当且仅当”。 – Elazar

@Elazar谢谢你。相应修改。 –

的Unicode在Coq的（≠）“不等于”符号

回答

相关问题