structure Lean.Elab.Term.MkInstResult : Type

• instVal : Lean.Expr
• instType : Lean.Expr
• outParams : Array Lean.Expr

Result for mkInst?

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

def Lean.Elab.DerivingHandler : Type

def Lean.Elab.DerivingHandlerNoArgs : Type

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

def Lean.Elab.registerDerivingHandlerWithArgs (className : Lake.Name) (handler : Lean.Elab.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.registerDerivingHandler (className : Lake.Name) (handler : Lean.Elab.DerivingHandlerNoArgs) : IO Unit

Like registerBuiltinDerivingHandlerWithArgs but ignoring any with argument.

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

def Lean.Elab.applyDerivingHandlers (className : Lake.Name) (typeNames : Array Lake.Name) (args? : Option (Lean.TSyntax `Lean.Parser.Term.structInst)) : Lean.Elab.Command.CommandElabM Unit

def Lean.Elab.elabDeriving : Lean.Elab.Command.CommandElab

structure Lean.Elab.DerivingClassView : Type

• ref : Lean.Syntax
• className : Lake.Name
• args? : Option (Lean.TSyntax `Lean.Parser.Term.structInst)

def Lean.Elab.getOptDerivingClasses {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadResolveName m] [Lean.MonadError m] [Lean.Elab.MonadInfoTree m] (optDeriving : Lean.Syntax) : m (Array Lean.Elab.DerivingClassView)

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