Documentation

Lean.Elab.Deriving.Util

source
def Lean.Elab.Deriving.implicitBinderF :
Lean.Parser.Parser
Equations
source
def Lean.Elab.Deriving.instBinderF :
Lean.Parser.Parser
Equations
source
def Lean.Elab.Deriving.explicitBinderF :
Lean.Parser.Parser
Equations
source
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✝].

Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
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}).

Equations
  • One or more equations did not get rendered due to their size.
source
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 α]).

Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Elab.Deriving.Context :
Type
Instances For
    source
    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.
    source
    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))
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Elab.Deriving.mkLet (letDecls : Array (Lean.TSyntax `Lean.Parser.Term.letDecl)) (body : Lean.Term) :
    Lean.Elab.TermElabM Lean.Term
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Elab.Deriving.mkInstanceCmds (ctx : Lean.Elab.Deriving.Context) (className : Lean.Name) (typeNames : Array Lean.Name) (useAnonCtor : optParam Bool true) :
    Lean.Elab.TermElabM (Array Lean.Command)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Elab.Deriving.mkDiscr (varName : Lean.Name) :
    Lean.Elab.TermElabM (Lean.TSyntax `Lean.Parser.Term.matchDiscr)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    structure Lean.Elab.Deriving.Header :
    Type
    Instances For
      source
      def Lean.Elab.Deriving.mkHeader (className : Lean.Name) (arity : Nat) (indVal : Lean.InductiveVal) :
      Lean.Elab.TermElabM Lean.Elab.Deriving.Header
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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.