Quelle bug_4294.v Sprache: Coq

Require Import TestSuite.hurkens.

Module NonPoly.
Module Type Foo.
  Definition U := Type.
  Parameter eq : Type = U.
End Foo.

Module M : Foo with Definition U := Type.
  Definition U := Type.
  Definition eq : Type = U := eq_refl.
End M.

Print Universes.
Fail Definition bad : False := TypeNeqSmallType.paradox M.U M.eq.
End NonPoly.

Set Universe Polymorphism.

Module Type Foo.
  Definition U := Type.
  Monomorphic Parameter eq : Type = U.
End Foo.

Module M : Foo with Definition U := Type.
  Definition U := Type.
  Monomorphic Definition eq : Type = U := eq_refl.
End M.

Fail Definition bad : False := TypeNeqSmallType.paradox Type M.eq.
(* Print Assumptions bad. *)

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.