mathlib3 documentation

core / init.meta.derive

meta def derive_handler  :

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 := bool.tt) (modify_target : name list expr expr tactic expr := λ (_x : name) (_x : list expr), has_pure.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 Type α] [a_3 : reflected Type β] :
has_reflect × β)
@[protected, instance]
@[protected, instance]
meta def sum.has_reflect (α : Type) [a : has_reflect α] (β : Type) [a_1 : has_reflect β] [a_2 : reflected Type α] [a_3 : reflected Type β] :
@[protected, instance]
meta def option.has_reflect (α : Type) [a : has_reflect α] [a_1 : reflected Type α] :
@[protected, instance]