Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_9595.v Sprache: Coq

Original von: Coq^©

Section foo.
Polymorphic Universes A B.
Fail Constraint A <= B.
End foo.
(* gives an anomaly Universe undefined *)

Universes X Y.
Section Foo.
  Polymorphic Universes Z W.
  Polymorphic Constraint W < Z.

  Fail Definition bla := Type@{W}.
  Polymorphic Definition bla := Type@{W}.
  Section Bar.
    Fail Constraint X <= Z.
  End Bar.
End Foo.

Require Coq.Classes.RelationClasses.

Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
{ refl : forall x, r x x }.

Section qux.
  Polymorphic Universes A.
  Section bar.
    Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
  End bar.
End qux.

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.