的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的（≠）「不等於」符號

回答

相關問題