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

• isCandidateFn : LetDecl Purity.pure → FVarIdSet → CompilerM Bool
• included : FVarIdSet

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

• toPull : Array (LetDecl Purity.pure)

@[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 Purity.pure)) (x : PullM α) : PullM α

@[inline]

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

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

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

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

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

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

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

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

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

def Lean.Compiler.LCNF.pullInstances : Pass