mathlib documentation


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  :
nametactic unit(bool := tt)(namelist exprexprtactic expr := λ (_x : name) (_x : list expr), 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.