mathlib3 documentation

core / init.meta.derive

source
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.

source
meta def derive_handler_attr  :
(user_attribute unit)
source
meta def derive_attr  :
user_attribute unit (list pexpr)
source
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) :
derive_handler

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.

source
meta def has_reflect_derive_handler  :
derive_handler
source
meta def has_sizeof_derive_handler  :
derive_handler
source
@[protected, instance]
meta def interactive.loc.has_reflect  :
has_reflect interactive.loc
source
@[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 (α × β)
source
@[protected, instance]
meta def bool.has_reflect  :
has_reflect bool
source
@[protected, instance]
meta def sum.has_reflect (α : Type) [a : has_reflect α] (β : Type) [a_1 : has_reflect β] [a_2 : reflected Type α] [a_3 : reflected Type β] :
has_reflect (α ⊕ β)
source
@[protected, instance]
meta def option.has_reflect (α : Type) [a : has_reflect α] [a_1 : reflected Type α] :
has_reflect (option α)
source
@[protected, instance]
meta def pos.has_reflect  :
has_reflect pos