Quelle bug_4816.v Sprache: Coq

#[universes(polymorphic)]
Section foo.
Polymorphic Universes A B.
Fail Monomorphic Constraint A <= B.
End foo.
(* gives an anomaly Universe undefined *)

Universes X Y.
#[universes(polymorphic)]
Section Foo.
  Polymorphic Universes Z W.
  Polymorphic Constraint W < Z.

  Fail Monomorphic Definition bla := Type@{W}.
  Polymorphic Definition bla := Type@{W}.
  #[universes(polymorphic)]
  Section Bar.
    Fail Monomorphic Constraint X <= Z.
  End Bar.
End Foo.

Axiom PreOrder : forall (A : Type) (r : A -> A -> Type), Type.

#[universes(polymorphic)]
Section qux.
  Polymorphic Universes A.
  #[universes(polymorphic)]
  Section bar.
    Fail Monomorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
  End bar.
End qux.

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.