Axiom X : Type. (* Used to declare [x0@{u1 u2} : X@{u1}] and [x1@{} : X@{u2}] leaving the type of x1 with undeclared universes. After PR #891 this should
error at declaration time. *) Axiom x₀ x₁ : X. Axiom Xᵢ : X -> Type.
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.
