1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Set Primitive Projections.
Class type (t : Type) : Type :=
{ bar : t -> Prop }.
#[export] Instance type_nat : type nat :=
{ bar := fun _ => True }.
Definition foo_bar {n : nat} : bar n := I.
#[local] Hint Resolve (@foo_bar) : typeclass_instances.
#[local] Hint Resolve I : typeclass_instances.
Check ltac:(typeclasses eauto with nocore typeclass_instances) : True.
Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
Existing Class bar.
Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
#[local] Hint Resolve (@foo_bar) : foo.
Check ltac:(typeclasses eauto with nocore typeclass_instances foo) : bar _.
|
