Zulip Chat Archive

Stream: lean4

Topic: deriving extensions


view this post on Zulip 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