blob: 0a52dcdef1b6f0719abb10db595132b1bafd77f2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.
Typeclasses eauto := debug.
Set Typeclasses Debug Verbosity 2.
Inductive Finx(n : nat) : Set :=
| Fx1(i : nat)(e : n = S i)
| FxS(i : nat)(f : Finx i)(e : n = S i).
Context `{Finx_eqdec : forall n, Eqdec (Finx n)}.
Goal {x : Type & Eqdec x}.
eexists.
try typeclasses eauto 1 with typeclass_instances.
Abort.
|
