|
Module A.
Set Printing All.
Set Printing Universes.
Module M.
Section foo.
Universe i.
End foo.
End M.
Check Type@{M.i}.
(* Succeeds *)
Fail Check Type@{j}.
(* Error: Undeclared universe: j *)
Definition foo@{j} : Type@{M.i} := Type@{j}.
(* ok *)
End A.
Import A. Import M.
Set Universe Polymorphism.
Fail Universes j.
Monomorphic Universe j.
Section foo.
Universes i.
Constraint i < j.
Definition foo : Type@{j} := Type@{i}.
Definition foo' : Type@{j} := Type@{i}.
End foo.
Check eq_refl : foo@{i} = foo'@{i}.
Definition bar := foo.
Monomorphic Definition bar'@{k} := foo@{k}.
Fail Constraint j = j.
Monomorphic Constraint i = 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.
|
