|
Set Universe Polymorphism.
Set Printing Universes.
Module GlobalReference.
Definition type' := Type.
Notation type := type'.
Check type@{Set}.
End GlobalReference.
Module TypeLiteral.
Notation type := Type.
Check type@{Set}.
Check type@{Prop}.
End TypeLiteral.
Module ExplicitSort.
Monomorphic Universe u.
Notation foo := Type@{u}.
Fail Check foo@{Set}.
Fail Check foo@{u}.
Notation bar := Type.
Check bar@{u}.
End ExplicitSort.
Module PropNotationUnsupported.
Notation foo := Prop.
Fail Check foo@{Set}.
Fail Check foo@{Type}.
End PropNotationUnsupported.
¤ Dauer der Verarbeitung: 0.18 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.
|
