A handler that may or may not be able to implement the typeclass cls
for decl
.
It should return tt
if it was able to derive cls
and ff
if it does not know
how to derive cls
, in which case lower-priority handlers will be tried next.
def
instance_derive_handler
(cls : name)
(tac : tactic unit)
(univ_poly : bool := tt)
(modify_target : name → list expr → expr → tactic expr := λ (_x : name) (_x : list expr), pure) :
Given a tactic tac
that can solve an application of cls
in the right context,
instance_derive_handler
uses it to build an instance declaration of cls n
.
@[instance]
def
prod.has_reflect
(α : Type)
[a : has_reflect α]
(β : Type)
[a_1 : has_reflect β]
[a_2 : reflected α]
[a_3 : reflected β] :
has_reflect (α × β)
@[instance]
def
sum.has_reflect
(α : Type)
[a : has_reflect α]
(β : Type)
[a_1 : has_reflect β]
[a_2 : reflected α]
[a_3 : reflected β] :
has_reflect (α ⊕ β)
@[instance]