blob: 4dee41e221b81154a71a7ca995692157519df8ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Classes.Init.
Class C A := c : A.
Instance nat_C : C nat := 0.
Instance bool_C : C bool := true.
Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
Proof. auto. Qed.
Goal True.
class_apply @silly; [reflexivity|].
reflexivity. Fail Qed.
|
