def Lean.Elab.Deriving.implicitBinderF : Lean.Parser.Parser

def Lean.Elab.Deriving.instBinderF : Lean.Parser.Parser

def Lean.Elab.Deriving.explicitBinderF : Lean.Parser.Parser

def Lean.Elab.Deriving.mkInductArgNames (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM (Array Lean.Name)

Make fresh, hygienic names for every parameter and index of an inductive declaration.

For example, inductive Foo {α : Type} : Nat → Type will give something like #[`α✝, `a✝].

def Lean.Elab.Deriving.mkInductiveApp (indVal : Lean.InductiveVal) (argNames : Array Lean.Name) : Lean.Elab.TermElabM Lean.Term

Return the inductive declaration's type applied to the arguments in argNames.

Equations

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

def Lean.Elab.Deriving.mkImplicitBinders (argNames : Array Lean.Name) : Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.implicitBinder))

Return implicit binder syntaxes for the given argNames. The output matches implicitBinder*.

For example, #[`foo,`bar] gives `({foo} {bar}).

def Lean.Elab.Deriving.mkInstImplicitBinders (className : Lean.Name) (indVal : Lean.InductiveVal) (argNames : Array Lean.Name) : Lean.Elab.TermElabM (Array Lean.Syntax)

Return instance binder syntaxes binding className α for every generic parameter α of the inductive indVal for which such a binding is type-correct. argNames is expected to provide names for the parameters (see mkInductArgNames). The output matches instBinder*.

For example, given inductive Foo {α : Type} (n : Nat) : (β : Type) → Type, where β is an index, invoking mkInstImplicitBinders `BarClass foo #[`α, `n, `β] gives `([BarClass α]).

structure Lean.Elab.Deriving.Context : Type

• typeInfos : Array Lean.InductiveVal
• auxFunNames : Array Lean.Name
• usePartial : Bool

def Lean.Elab.Deriving.mkContext (fnPrefix : String) (typeName : Lean.Name) : Lean.Elab.TermElabM Lean.Elab.Deriving.Context

Equations

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

def Lean.Elab.Deriving.mkLocalInstanceLetDecls (ctx : Lean.Elab.Deriving.Context) (className : Lean.Name) (argNames : Array Lean.Name) : Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.letDecl))

def Lean.Elab.Deriving.mkLet (letDecls : Array (Lean.TSyntax `Lean.Parser.Term.letDecl)) (body : Lean.Term) : Lean.Elab.TermElabM Lean.Term

def Lean.Elab.Deriving.mkInstanceCmds (ctx : Lean.Elab.Deriving.Context) (className : Lean.Name) (typeNames : Array Lean.Name) (useAnonCtor : Bool := true) : Lean.Elab.TermElabM (Array Lean.Command)

Equations

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

def Lean.Elab.Deriving.mkDiscr (varName : Lean.Name) : Lean.Elab.TermElabM (Lean.TSyntax `Lean.Parser.Term.matchDiscr)

structure Lean.Elab.Deriving.Header : Type

• binders : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
• argNames : Array Lean.Name
• targetNames : Array Lean.Name
• targetType : Lean.Term

def Lean.Elab.Deriving.mkHeader (className : Lean.Name) (arity : Nat) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM Lean.Elab.Deriving.Header

def Lean.Elab.Deriving.mkDiscrs (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchDiscr))

Equations

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