|
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.119 Sekunden
(vorverarbeitet)
¤
|
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.
|
