Print Universes Subgraph(i j). (* should print [i < j], not [l < k] (and not prelude universes) *)
Definition connect : Type@{l} := Type@{j}.
Print Universes Subgraph (i k).
Universes u v. ModuleType T. Definition foo : Type@{u} := Type@{v}. End T.
Print Universes Subgraph (u v). (* T.foo does not exist but we don't fail *)
Messung V0.5 in Prozent
¤ 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.0.9Bemerkung:
(vorverarbeitet am 2026-09-29)
¤
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 und die Messung sind noch experimentell.
