Unicode notation "Different" en Coq (≠)

Le texte suivant est mentionné dans le livre SF:Unicode notation "Different" en Coq (≠)

Voici comment nous utilisons ne pas dire que 0 et 1 sont différents éléments de 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 *) 

Mais quand je fait cela en Coq:

Il me donne cette erreur:

Syntax Error: Lexer: Undefined token

En fait, en regardant le standard library, je ne peux pas trouver de notation pour cela. Quelle est la notation appropriée pour cela?

Source

2017-04-02 Sibi

Vous n'êtes pas familier avec Coq typé langue, mais en regardant la bibliothèque standard, sûrement _pas égale to_ serait '<>' 'ou' <->? –

@JonathonOgden Oui, vous avez raison. C'est '<>'. J'ai regardé cela mais ignoré car c'était l'opération sur les monoïdes. :) Pouvez-vous poster cela comme une réponse? – Sibi

Terminé. Nous vous recommandons également de voir @Elazar réponse. Logique. –

Check 1 <> 2.

Mais vous pouvez aussi le faire:

Require Import Unicode.Utf8. 
Check 1 ≠ 2.

Source

2017-04-02 21:46:33 Elazar

Pas familier avec le langage typé Coq, mais en regardant la bibliothèque standard, pas égal à serait écrit comme <>. Comme le dit @jonathon, l'opérateur est écrit <>

Source

2017-04-02 21:42:42

'<->' est "Si et seulement si". – Elazar

@Elazar merci. Modifié en conséquence. –

Unicode notation "Different" en Coq (≠)

Répondre

Questions connexes