Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: universes3.v Sprache: Coq

Original von: Coq^©

(* This example (found by coqchk) checks that an inductive cannot be
   polymorphic if its constructors induce upper universe constraints.
   Here: I cannot be polymorphic because its type is less than the
   type of the argument of impl. *)

Definition Type1 := Type.
Definition Type3 : Type1 := Type.                       (* Type3 < Type1 *)
Definition Type4 := Type.
Definition impl (A B:Type3) : Type4 := A->B.           (* Type3 <= Type4 *)
Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B).
    (* Type(6) <= Type(7)     because I contains, via C, elements in B
       Type(7) <=  Type3      because (I B) is argument of impl
       Type(4) <=  Type(7)    because type of C less than I (see remark below)

       where Type(7) is the auxiliary level used to infer the type of I
*)

(* We cannot enforce Type1 < Type(6) while we already have
   Type(6) <= Type(7) < Type3 < Type1 *)
Fail Definition J := I Type1.

(* Open question: should the type of an inductive be the max of the
   types of the _arguments_ of its constructors (here B and Prop,
   after unfolding of impl), or of the max of types of the
   constructors itself (here B -> impl Prop (I B)), as done above. *)

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.