blob: c2debdecfe25038d6dfb38dc1a3d9ffbd1768c87 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Axiom P : nat -> Prop.
Class class (A : Type) := { val : A }.
Lemma usetc {t : class nat} : P (@val nat t).
Admitted.
Notation "{val:= v }" := (@val _ v).
Instance zero : class nat := {| val := 0 |}.
Lemma test : P 0.
Fail apply usetc.
pose (tmp := usetc); apply tmp; clear tmp.
Qed.
|
