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

Equations

• Lean.Elab.Deriving.implicitBinderF = Lean.Parser.Term.implicitBinder

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

Equations

• Lean.Elab.Deriving.instBinderF = Lean.Parser.Term.instBinder

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

Equations

• Lean.Elab.Deriving.explicitBinderF = Lean.Parser.Term.explicitBinder

def Lean.Elab.Deriving.mkInductArgNames (indVal : InductiveVal) : TermElabM (Array 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✝].

Equations

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

def Lean.Elab.Deriving.mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM 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 Name) : TermElabM (Array (TSyntax `Lean.Parser.Term.implicitBinder))

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

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

Equations

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

def Lean.Elab.Deriving.mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array 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 α]).

Equations

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

def Lean.Elab.Deriving.withoutExposeFromCtors {α : Type} (typeName : Name) (cont : Command.CommandElabM α) : Command.CommandElabM α

Removes any [expose] section attributes when running cont if typeName has private ctors.

Equations

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

structure Lean.Elab.Deriving.Context : Type

• instName : Name
• typeInfos : Array InductiveVal
• auxFunNames : Array Name
• usePartial : Bool

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

structure Lean.Elab.Deriving.Header : Type

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

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

Equations

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

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

Equations

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