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

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)

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).

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.elabDeriving : Command.CommandElab

Equations

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

structure Lean.Elab.DerivingClassView : Type

• ref : Syntax
• className : Name

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

Equations

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

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

Equations

• view.applyHandlers declNames = Lean.withRef view.ref (Lean.Elab.applyDerivingHandlers view.className declNames)