(* 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. *)
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.
