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". *)
Messung V0.5
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤
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 und die Messung sind noch experimentell.