|
Set Universe Polymorphism.
Section foo.
Universe i.
Context (foo : Type@{i}) (bar : Type@{i}).
Definition qux@{i} (baz : Type@{i}) := foo -> bar.
End foo.
Set Printing Universes.
Print qux. (* qux@{Top.42 Top.43} =
fun foo bar _ : Type@{Top.42} => foo -> bar
: Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42}
(* Top.42 Top.43 |= *)
(* This is wrong; the first two types are equal, but the last one is not *)
qux is universe polymorphic
Argument scopes are [type_scope type_scope type_scope]
*)
Check qux nat nat nat : Set.
Check qux nat nat Set : Set. (* Error:
The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is
expected to have type "Set"
(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
¤ 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.
|
