(* File reduced by coq-bug-finder from original input, then from 1829 lines to 37 lines, then from 47 lines to 18 lines *)
Class Contr_internal (A : Type) :=
BuildContr { center : A ;
contr : (forall y : A, True) }. Class Contr A := Contr_is_contr : Contr_internal A. Inductive Unit : Set := tt.
#[export] Instance contr_unit : Contr Unit | 0 := let x := {|
center := tt;
contr := fun t : Unit => I
|} in x. (* success *)
#[export] Instance contr_internal_unit' : Contr_internal Unit | 0 :=
{|
center := tt;
contr := fun t : Unit => I
|}.
#[export] Instance contr_unit' : Contr Unit | 0 :=
{|
center := tt;
contr := fun t : Unit => I
|}. (* Error: Mismatched contexts while declaring instance: Expected: (Contr_is_contr : Contr_internal _UNBOUND_REL_1)
Found: tt (fun t : Unit => I) *)
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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.
