|
Set Printing Universes.
Definition foo : Type.
Proof.
assert (H : Set) by abstract (assert Type by abstract exact Type 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}". *)
¤ Dauer der Verarbeitung: 0.15 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.
|
