structure Lean.Elab.Term.MkInstResult : Type

Result for mkInst?

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

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.DerivingHandler : Type

Equations

• Lean.Elab.DerivingHandler = (Array Lean.Name → Lean.Elab.Command.CommandElabM Bool)

@[deprecated Lean.Elab.DerivingHandler]

def Lean.Elab.DerivingHandlerNoArgs : Type

Deprecated - DerivingHandler no longer assumes arguments

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

def Lean.Elab.registerDerivingHandler (className : Lean.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.defaultHandler (className : Lean.Name) (typeNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Unit

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.DerivingClassView : Type

• ref : Lean.Syntax
• className : Lean.Name

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

Equations

• One or more equations did not get rendered due to their size.

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