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
31
32
33
|
Record myRecord := {
my_class : Type ;
}.
Fail #[export] Instance my_instance : forall x, my_class x.
Existing Class my_class.
#[export] Instance my_instance : forall x, my_class x. Abort.
Definition my_existing_instance : forall x, my_class x. Admitted.
#[export]
Existing Instance my_existing_instance.
Set Primitive Projections.
Record myOtherRecord := {
my_other_class : Type ;
}.
Fail #[export] Instance my_other_instance : forall x, my_other_class x.
Existing Class my_other_class.
#[export] Instance my_other_instance : forall x, my_other_class x. Abort.
Definition my_other_existing_instance : forall x, my_other_class x. Admitted.
(* ??? *)
(* Used to be: Constant does not build instances of a declared type class. *)
#[export]
Existing Instance my_other_existing_instance.
|
