|
Set Universe Polymorphism.
Module OK.
Inductive one@{i j} : Type@{i} :=
with two : Type@{j} := .
Check one@{Set Type} : Set.
Fail Check two@{Set Type} : Set.
End OK.
Module Bad.
Fail Inductive one :=
with two@{i +} : Type@{i} := .
Fail Inductive one@{i +} :=
with two@{i +} := .
End Bad.
¤ Dauer der Verarbeitung: 0.16 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.
|
