Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_3439.v Sprache: Coq

Original von: Coq^©

Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 3154 lines to 149 lines, then from 89 lines to 55 lines, then from 44 lines to 20 lines *)
Set Primitive Projections.
Generalizable All Variables.
Axiom IsHSet : Type -> Type.
Existing Class IsHSet.
Record PreCategory := { object :> Type }.
Notation IsStrictCategory C := (IsHSet (object C)).
Instance trunc_prod `{IsHSet A} `{IsHSet B} : IsHSet (A * B) | 100.
admit.
Defined.
Typeclasses Transparent object.
Definition prod (C D : PreCategory) : PreCategory := Build_PreCategory (Datatypes.prod C D).
Global Instance isstrict_category_product `{IsStrictCategory C, IsStrictCategory D} : IsStrictCategory (prod C D).
Proof.
  typeclasses eauto.
Defined.

Set Typeclasses Debug.
(* File reduced by coq-bug-finder from original input, then from 7425 lines to 154 lines, then from 116 lines to 20 lines *)
Class Contr (A : Type) := { center : A }.
Instance contr_unit : Contr unit | 0 := {| center := tt |}.
Module non_prim.
  Unset Primitive Projections.
  Record PreCategory := { object :> Type }.
  Lemma foo : Contr (object (@Build_PreCategory unit)).
  Proof.
    solve [ simpl; typeclasses eauto ] || fail "goal not solved".
    Undo.
    solve [ typeclasses eauto ].
  Defined.
End non_prim.

Module prim.
  Set Primitive Projections.
  Record PreCategory := { object :> Type }.
  Lemma foo : Contr (object (@Build_PreCategory unit)).
  Proof.
    solve [ simpl; typeclasses eauto ] || fail "goal not solved".
    Undo.
    solve [ typeclasses eauto ]. (*  Error: No applicable tactic. *)
  Defined.
End prim.

¤ Dauer der Verarbeitung: 0.23 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.