## Stream: lean4

### Topic: deriving extensions

#### Leonardo de Moura (Jan 25 2021 at 04:20):

Users will be able to extend deriving for their own classes. However, deriving is a relatively new feature, and the API is not stable and there are missing features. That being said, users should be able to invoke registerBuiltinDerivingHandler from their plugins. You can build a plugin containing

def mkMyClassInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
...

initialize
registerBuiltinDerivingHandler MyClass mkMyClassInstanceHandler


Disclaimer: we do not have many tests for Lean 4 plugins yet, and we never extended deriving using plugins :(
We have a very simple plugin at lean4/tests/plugin`.

Last updated: May 18 2021 at 23:14 UTC