Lean.Elab.Deriving.Basic

source

def Lean.Elab.DerivingHandler:

Type

Equations

Lean.Elab.DerivingHandler = (Array Lean.Name → Option (Lean.TSyntax `Lean.Parser.Term.structInst) → Lean.Elab.Command.CommandElabM Bool)

source

def Lean.Elab.DerivingHandlerNoArgs:

Type

Equations

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

source

opaque Lean.Elab.derivingHandlersRef:

IO.Ref (Lean.NameMap Lean.Elab.DerivingHandler)

source

def Lean.Elab.registerBuiltinDerivingHandlerWithArgs (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).

Equations

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

source

def Lean.Elab.registerBuiltinDerivingHandler (className : Lean.Name) (handler : Lean.Elab.DerivingHandlerNoArgs) :

IO Unit

Like registerBuiltinDerivingHandlerWithArgs but ignoring any with argument.

Equations

Lean.Elab.registerBuiltinDerivingHandler className handler = Lean.Elab.registerBuiltinDerivingHandlerWithArgs className fun typeNames x => handler typeNames

source

def Lean.Elab.defaultHandler (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.

source

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

Lean.Elab.Command.CommandElabM Unit

Equations

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

source

def Lean.Elab.elabDeriving:

Lean.Elab.Command.CommandElab

Equations

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

source

structure Lean.Elab.DerivingClassView:

Type

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

source

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

m (Array Lean.Elab.DerivingClassView)

Equations

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

source

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

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.DerivingClassView.applyHandlers view declNames = Lean.withRef view.ref (Lean.Elab.applyDerivingHandlers view.className declNames view.args?)