structure Lean.Compiler.LCNF.PullLetDecls.Context : Type

• isCandidateFn : LetDecl → FVarIdSet → CompilerM Bool
• included : FVarIdSet

structure Lean.Compiler.LCNF.PullLetDecls.State : Type

• toPull : Array LetDecl

@[reducible, inline]

abbrev Lean.Compiler.LCNF.PullLetDecls.PullM (α : Type) : Type

@[inline]

def Lean.Compiler.LCNF.PullLetDecls.withFVar {α : Type} (fvarId : FVarId) (x : PullM α) : PullM α

@[inline]

def Lean.Compiler.LCNF.PullLetDecls.withParams {α : Type} (ps : Array Param) (x : PullM α) : PullM α

@[inline]

def Lean.Compiler.LCNF.PullLetDecls.withNewScope {α : Type} (x : PullM α) : PullM α

def Lean.Compiler.LCNF.PullLetDecls.withCheckpoint (x : PullM Code) : PullM Code

partial def Lean.Compiler.LCNF.PullLetDecls.withCheckpoint.go (c : Code) (toPull : Array LetDecl) (i : Nat) (included : FVarIdSet) : StateM (Array LetDecl) Code

def Lean.Compiler.LCNF.PullLetDecls.attachToPull (c : Code) : PullM Code

def Lean.Compiler.LCNF.PullLetDecls.shouldPull (decl : LetDecl) : PullM Bool

partial def Lean.Compiler.LCNF.PullLetDecls.pullAlt (alt : Alt) : PullM Alt

partial def Lean.Compiler.LCNF.PullLetDecls.pullDecls (code : Code) : PullM Code

def Lean.Compiler.LCNF.PullLetDecls.PullM.run {α : Type} (x : PullM α) (isCandidateFn : LetDecl → FVarIdSet → CompilerM Bool) : CompilerM α

def Lean.Compiler.LCNF.Decl.pullLetDecls (decl : Decl) (isCandidateFn : LetDecl → FVarIdSet → CompilerM Bool) : CompilerM Decl

def Lean.Compiler.LCNF.Decl.pullInstances (decl : Decl) : CompilerM Decl

def Lean.Compiler.LCNF.pullInstances : Pass