|
Set Universe Polymorphism.
Definition hProp : Type := sigT (fun _ : Type => True).
Goal Type.
Fail exact hProp@{Set}. (* test that it fails, but is not an anomaly *)
try (exact hProp@{Set}; fail 1). (* Toplevel input, characters 15-32:
Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
Please report. *)
Abort.
¤ Dauer der Verarbeitung: 0.35 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.
|
