|
Set Universe Polymorphism.
Set Printing Universes.
Axiom foo@{i j} : Type@{i} -> Type@{j}.
Notation bar := foo.
Monomorphic Universes i j.
Check bar@{i j}.
Fail Check bar@{i}.
Notation qux := (nat -> nat).
Fail Check qux@{i}.
Axiom TruncType@{i} : nat -> Type@{i}.
Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
Notation hProp := (0)-Type.
Check hProp.
Check hProp@{i}.
¤ Dauer der Verarbeitung: 0.13 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.
|
