|
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.*)
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.27Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
