# Documentation

Lean.Compiler.LCNF.PullFunDecls

Local function declaration and join point being pulled.

Instances For
Equations
@[inline]

The PullM state contains the local function declarations and join points being pulled.

Equations

Extract from the state any local function declarations that depends on the given free variable. The idea is that we have to stop pulling these declarations because they depend on fvarId.

Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• = do let ps ←

Similar to findFVarDeps. Extract from the state any local function declarations that depends on the given parameters.

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

Construct the code fun p.decl k or jp p.decl k.

Equations

Attach the given array of local function declarations and join points to k.

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.
Equations
• = do let __do_lift ← get pure __do_lift.snd[i]!

Extract from the state any local function declarations that depends on the given free variable, and attach to code k.

Equations
• = do let ps ←

Similar to attachFVarDeps. Extract from the state any local function declarations that depends on the given parameters, and attach to code k.

Equations
• = do let ps ←
Equations
• One or more equations did not get rendered due to their size.

Add local function declaration (or join point if isFun = false) to the state.

Pull local function declarations and join points in code. The state contains the declarations being pulled.

Pull local function declarations and join points in the given declaration.

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