(*
I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *)
*)
(* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive Empty : Set := .
Record IsHProp (A : Type) := { foo : True }. Definition hprop_Empty : IsHProp@{i} Empty := {| foo := I |}. Goallet U := Type in let gt := Set : U in IsHProp (Empty : U). simpl. Set Printing Universes. exact @hprop_Empty. (* Toplevel input, characters 21-32: Error:
The term "hprop_Empty" has type "IsHProp (* Set *)
while it is expected to have type"IsHProp (* Top.17 *) Empty"
(Universe inconsistency: Cannot enforce Top.17 = Set because Set < Top.17)). *) Defined.
Module B. (* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where"x = y" := (@paths _ x y) : type_scope.
Record Contr (A : Type) := { center : A }.
Monomorphic Record IsHProp (A : Type) := { foo : forall x y : A, Contr (x = y) }. Definition hprop_Empty : IsHProp Empty := {| foo x y := match x : Empty withend |}. Goallet U := Type in let gt := Set : U in IsHProp (Empty : U). simpl. Set Printing Universes. exact hprop_Empty. Defined. End B.
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.
