Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: rl115a.cob Sprache: Coq

Original von: Coq^©

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.32 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.