structure Lean.Elab.DerivingClassView : Type

• ref : Syntax
• hasExpose : Bool
• cls : Term

def Lean.Elab.Term.processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit

Delta deriving handler. Creates an instance of class classStx for decl. The elaborated class expression may be underapplied (e.g. Decidable instead of Decidable _), and may be decl. If unfolding decl results in an underapplied lambda, then this enters the body of the lambda. We prevent classStx from referring to these local variables; instead it's expected that one uses section variables.

This function can handle being run from within a nontrivial local context, and it uses mkValueTypeClosure to construct the final instance.

def Lean.Elab.DerivingHandler : Type

opaque Lean.Elab.derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler))

def Lean.Elab.registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit

Registers a deriving handler for a class. This function should be called in an initialize block.

A DerivingHandler is called on the fully qualified names of all types it is running for. For example, deriving instance Foo for Bar, Baz invokes fooHandler #[`Bar, `Baz].

def Lean.Elab.applyDerivingHandlers (className : Name) (typeNames : Array Name) (setExpose : Bool := false) : Command.CommandElabM Unit

def Lean.Elab.DerivingClassView.getClassName (view : DerivingClassView) : CoreM Name

def Lean.Elab.DerivingClassView.ofSyntax : TSyntax `Lean.Parser.Command.derivingClass → CoreM DerivingClassView

def Lean.Elab.getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView)

def Lean.Elab.DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : Command.CommandElabM Unit

def Lean.Elab.elabDeriving : Command.CommandElab