structure Lean.Elab.Term.MkInstResult : Type

Result for mkInst?

• instVal : Expr
• instType : Expr
• outParams : Array Expr

def Lean.Elab.Term.processDefDeriving (className declName : Name) : TermElabM Bool

def Lean.Elab.DerivingHandler : Type

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

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

A DerivingHandler is called on the fully qualified names of all types it is running for as well as the syntax of a with argument, if present.

For example, deriving instance Foo with fooArgs for Bar, Baz invokes fooHandler #[`Bar, `Baz] `(fooArgs).

def Lean.Elab.defaultHandler (className : Name) (typeNames : Array Name) : Command.CommandElabM Unit

def Lean.Elab.applyDerivingHandlers (className : Name) (typeNames : Array Name) : Command.CommandElabM Unit

def Lean.Elab.elabDeriving : Command.CommandElab

structure Lean.Elab.DerivingClassView : Type

• ref : Syntax
• className : Name

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

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