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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
structure Lean.Elab.Deriving.Context :
Type

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

Instances For

source
def Lean.Elab.Deriving.mkInstName (className indName : Name) :
TermElabM Name

Anticipates the default instance name for a derived instance.

Equations

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

Instances For

source
def Lean.Elab.Deriving.mkContext (className : Name) (fnPrefix : String) (typeName : Name) (supportsRec : Bool := true) :
TermElabM Context
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
structure Lean.Elab.Deriving.Header :
Type

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

Instances For

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

Instances For

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

Instances For