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]