# Documentation

Lean.Compiler.LCNF.LambdaLifting

• If liftInstParamOnly is true, then only local functions that take local instances as parameters are lambda lifted.

liftInstParamOnly : Bool
• Suffix for the new auxiliary declarations being created.

suffix : Lean.Name
• Declaration where lambda lifting is being applied. We use it to provide the "base name" for auxiliary declarations and the flag safe.

• If true, the lambda-lifted functions inherit the inline attribute from mainDecl. We use this feature to implement @[inline] instance ... and @[always_inline] instance ...

inheritInlineAttrs : Bool
• Only local functions with size > minSize are lambda lifted. We use this feature to implement @[inline] instance ... and @[always_inline] instance ...

minSize : Nat

Context for the LiftM monad.

Instances For
• New auxiliary declarations

decls :
• Next index for generating auxiliary declaration name.

nextIdx : Nat

State for the LiftM monad.

Instances For
@[inline]

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

Return true if the given declaration takes a local instance as a parameter. We lambda lift this kind of local function declaration before specialization.

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

Return true if the given declaration should be lambda lifted.

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

Create a new auxiliary declaration. The array closure contains all free variables occurring in decl.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.LambdaLifting.mkAuxDecl.go (closure : ) (decl : Lean.Compiler.LCNF.FunDecl) (nameNew : Lean.Name) (safe : Bool) (inlineAttr? : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Compiler.LCNF.Decl.lambdaLifting (decl : Lean.Compiler.LCNF.Decl) (liftInstParamOnly : Bool) (suffix : Lean.Name) (inheritInlineAttrs : ) (minSize : ) :
Equations
• One or more equations did not get rendered due to their size.

Eliminate all local function declarations.

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

During eager lambda lifting, we lift

• All local function declarations from instances (motivation: make sure it is cheap to inline them later)
• Local function declarations that take local instances as parameters (motivation: ensure they are specialized)
Equations
• One or more equations did not get rendered due to their size.