(* To anticipate that obligations may declare universes, we require
extensibility of the universe declaration for Program defintiions *)
Fail ProgramDefinition foo@{u} : Type@{u} := _.
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.
