Set Printing Universes. Definition foo : Type. Proof. assert (H : Set) by abstract (assertTypeby abstract exactType using bar; exact nat). exact bar. Defined. (* Toplevel input, characters 0-8: Error: The term "(fun _ : Set => bar) foo_subproof" has type
"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *)
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.
