Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_5011.v Sprache: Coq

Original von: Coq^©

Notation "P |-- Q" := (@eq nat P Q) (at level 80, Q at level 41, no associativity) .
Notation "x &&& y" := (plus x y) (at level 40, left associativity, y at next level) .
Notation "'Ex' x , P " := (plus x P) (at level 65, x at level 99, P at level 80).

(* Succeed *)
Check _ |-- _ &&& _ -> _.
Check _ |-- _ &&& (Ex _, _ ) -> _.
Check _ |-- (_ &&& Ex _, _ ) -> _.

(* Why does this fail? *)
Fail Check _ |-- _ &&& Ex _, _  -> _.
(* The command has indeed failed with message:
=> Error: The term "Ex ?17, ?18" has type "nat"
which should be Set, Prop or Type. *)

(* Just in case something is strange with -> *)
Notation "P ----> Q" := (P -> Q) (right associativity, at level 99, Q at next level).

(* Succeed *)
Check _ |-- _ &&& _ ----> _.
Check _ |-- _ &&& (Ex _, _ )  ----> _.
Check _ |-- (_ &&& Ex _, _ )  ----> _.

(* Why does this fail? *)
Fail Check _ |-- _ &&& Ex _, _  ----> _.
(* The command has indeed failed with message:
=> Error: The term "Ex ?31, ?32" has type "nat"
which should be Set, Prop or Type.*)

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.