blob: 1ea24bf1b84920a05e60fb1653a26cf46bfd3fbf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
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.
|
