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
|
Set Implicit Arguments.
Generalizable Variables A B.
Parameter val: Type.
Class Enc (A:Type) : Type :=
make_Enc { enc : A -> val }.
Hint Mode Enc + : typeclass_instances.
Parameter bar : forall A (EA:Enc A), EA = EA.
Parameter foo : forall (P:Prop),
P ->
P = P ->
True.
Parameter id : forall (P:Prop),
P -> P.
Check enc.
Lemma test : True.
eapply foo; [ eapply bar | apply id]. apply id.
(* eapply bar introduces an unresolved typeclass evar that is no longer
a candidate after the application (eapply should leave typeclass goals shelved).
We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`..
*)
Abort.
|
