Quellcode-Bibliothek bug_15916.v Sprache: Coq

Set Universe Polymorphism. Set Printing Universes.

Module MultiInd.
  Section S.
    Universe u.

    Cumulative Inductive I1 := C1 (_:Type@{u}).

    Cumulative Inductive I2 := C2 (_:I1).
  End S.

  (* !!! should be covariant !!! *)
  Fail Cumulative Inductive I3@{*u} := C3 (_:I2@{u}).

  Cumulative Inductive I3@{u} := C3 (_:I2@{u}).

  (* alternative test without the variance syntax: *)
  Fail Check C3@{Type} _ : I3@{Set}. (* should fail but doesn't *)

  Check C3@{Set} _ : I3@{Type}.
End MultiInd.

Module WithAxiom.
  Section S.
    Universe u.
    Axiom t : Type@{u}. (* or even a Qed definition *)

    Cumulative Inductive I1 := C1 (_:t).
  End S.

  (* !!! should be invariant !!! *)
  Fail Cumulative Inductive I2@{*u} := C2 (_:I1@{u}).
  Fail Cumulative Inductive I2@{+u} := C2 (_:I1@{u}).
  Cumulative Inductive I2@{u} := C2 (_:I1@{u}).

  (* !!! should not work !!! *)
  Fail Polymorphic Definition lift_t@{u v|} (x:t@{u}) : t@{v}
    := match (C1@{u} x) : I1@{v} with C1 y => y end.
  Fail Polymorphic Definition lift_t@{u v|u < v +} (x:t@{u}) : t@{v}
    := match (C1@{u} x) : I1@{v} with C1 y => y end.

  (* sanity check that the above 2 test the right thing *)
  Polymorphic Definition lift_t@{u v} (x:t@{u}) : t@{v}
    := match (C1@{u} x) : I1@{v} with C1 y => y end.

End WithAxiom.

Module WithVars.

  Module Rel.
    Fail Cumulative Inductive foo@{*u +} (X:=Type@{u}) := C (_:X).

    Cumulative Inductive foo@{+u +} (X:=Type@{u}) := C (_:X).
  End Rel.

  Module Var.
    Section S.
      Let X:=Type.
      Cumulative Inductive foo := C (_:X).
    End S.

    Fail Cumulative Inductive bar@{*u} := C' (_:foo@{u}).
    Cumulative Inductive bar@{+u} := C' (_:foo@{u}).
  End Var.

End WithVars.

quality100%

¤ 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.0.14Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.