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 : Lake.Name) (declName : Lake.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 Lake.Name → Option (Lean.TSyntax `Lean.Parser.Term.structInst) → Lean.Elab.Command.CommandElabM Bool)

def Lean.Elab.DerivingHandlerNoArgs : Type

Equations

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

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

Equations

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

def Lean.Elab.registerDerivingHandler (className : Lake.Name) (handler : Lean.Elab.DerivingHandlerNoArgs) : IO Unit

Like registerBuiltinDerivingHandlerWithArgs but ignoring any with argument.

Equations

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

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

Equations

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

def Lean.Elab.applyDerivingHandlers (className : Lake.Name) (typeNames : Array Lake.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.

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

Equations

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

def Lean.Elab.DerivingClassView.applyHandlers (view : Lean.Elab.DerivingClassView) (declNames : Array Lake.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?)