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
|
Require Import Classes.DecidableClass.
Inductive Foo : Set :=
| foo1 | foo2.
Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
Proof.
intros P H.
refine (Build_Decidable _ (if H then true else false) _).
intuition congruence.
Qed.
#[export] Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances.
Goal forall (a b : Foo), {a=b}+{a<>b}.
intros.
abstract (abstract (decide equality)). (*abstract works here*)
Qed.
Check ltac:(abstract (exact I)) : True.
Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
intros.
split. typeclasses eauto.
typeclasses eauto. Qed.
Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
intros.
split.
refine _.
refine _.
Defined.
(*fails*)
|
