mathlib documentation

core / init.meta.derive

meta def derive_handler  :
Type

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.

meta def instance_derive_handler (cls : name) (tac : tactic unit) (univ_poly : bool := tt) (modify_target : namelist exprexprtactic 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.

@[protected, instance]
@[protected, instance]
meta def prod.has_reflect (α : Type) [a : has_reflect α] (β : Type) [a_1 : has_reflect β] [a_2 : reflected α] [a_3 : reflected β] :
has_reflect × β)
@[protected, instance]
@[protected, instance]
meta def sum.has_reflect (α : Type) [a : has_reflect α] (β : Type) [a_1 : has_reflect β] [a_2 : reflected α] [a_3 : reflected β] :
@[protected, instance]
meta def option.has_reflect (α : Type) [a : has_reflect α] [a_1 : reflected α] :
@[protected, instance]