- isFun : Bool
- decl : Lean.Compiler.LCNF.FunDecl
- used : Lean.FVarIdSet
Local function declaration and join point being pulled.
Instances For
The PullM
state contains the local function declarations and join points being pulled.
Instances For
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
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.PullFunDecls.findFVarDirectDeps.go fvarId [] keep dep = pure (keep, dep)
Instances For
Similar to findFVarDeps
. Extract from the state any local function declarations that depends on the given
parameters.
Instances For
Construct the code fun p.decl k
or jp p.decl k
.
Instances For
Attach the given array of local function declarations and join points to k
.
Instances For
Instances For
Instances For
Extract from the state any local function declarations that depends on the given
free variable, and attach to code k
.
Instances For
Similar to attachFVarDeps
. Extract from the state any local function declarations that depends on the given
parameters, and attach to code k
.
Instances For
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.