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.
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.
