blob: decddb73d154df80ca37efbe1521f28d2a7322fe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Module Postponing.
Class In A T := { IsIn : A -> T -> Prop }.
Class Empty T := { empty : T }.
Class EmptyIn (A T : Type) `{In A T} `{Empty T} :=
{ isempty : forall x, IsIn x empty -> False }.
Hint Mode EmptyIn ! ! - - : typeclass_instances.
Hint Mode Empty ! : typeclass_instances.
Hint Mode In ! - : typeclass_instances.
Existing Class IsIn.
Goal forall A T `{In A T} `{Empty T} `{EmptyIn A T}, forall x : A, IsIn x empty -> False.
Proof.
intros.
eapply @isempty. (* Second goal needs to be solved first, to un-stuck the first one
(hence the Existing Class IsIn to allow finding the assumption of IsIn here) *)
all:typeclasses eauto.
Qed.
End Postponing.
|
