How to elable `deriving` for user defined type class

Stream: new members

[Asei Inoue]

/-- user defined type class -/
class Callable (α : Type) where
  call : α → String

/--
error: default handlers have not been implemented yet, class: 'Deriving.Callable' types: [Deriving.People]
-/
#guard_msgs in
deriving instance Callable for People

[Asei Inoue]

Can I define my own deriving procedure for an arbitrary typeclass?

[Kyle Miller]

I think the only reference for that is to look at pre-existing derive handlers. You can search for registerDerivingHandler in Lean and mathlib.

[Adam Topaz]

Here's the source for the handler for Nonempty, for example: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/Nonempty.lean

[Adam Topaz]

That folder has a few other examples.