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
.