Unset Strict Universe Declaration.
Set Universe Polymorphism.
Module Type Foo.
Parameter U : Type.
End Foo.
Module Lower (X : Foo with Definition U := True : Type).
End Lower.
Module M : Foo.
Definition U := nat : Type@{i}.
End M.
¤ Dauer der Verarbeitung: 0.16 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.
|