blob: d6d3021200f478d01f575f3945bbacdeef7e93d9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
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.
Abort.
|
