Set Printing Universes. Local Close Scope nat_scope. Check (fun ab : Prop * Prop => (fst ab : Prop) * (snd ab : Prop)). (* fun ab : Prop * Prop =>
(fst (* Top.5817 Top.5818 *)
: Prop * Prop -> Prop *) Check (fun ab : Prop * Prop => (fst ab : Prop) * (snd ab : Prop) : Prop). (* Toplevel input, characters 51-84: Error: In environment ab : Prop * Prop The term
"(fst (* Top.5833 Top.5834 *)
(snd (* Top.5833 Top.5834 *) ab:Prop)" has type "Type (* max(Top.5829, Top.5830) *)" while it is expected to have type "Prop". *)
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.
