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.

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

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

Equations

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

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

Equations

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

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

Equations

• view.getClassName = Lean.Elab.realizeGlobalConstNoOverloadWithInfo view.cls.raw

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

Equations

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

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 do let __do_lift ← Lean.Elab.Command.liftCoreM view.getClassName Lean.Elab.applyDerivingHandlers __do_lift declNames view.hasExpose

def Lean.Elab.elabDeriving : Command.CommandElab

Equations

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