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

Equations

• Lean.Compiler.LCNF.PullLetDecls.PullM = ReaderT Lean.Compiler.LCNF.PullLetDecls.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.PullLetDecls.State Lean.Compiler.LCNF.CompilerM)

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Compiler.LCNF.PullLetDecls.withNewScope x = withReader (fun (ctx : Lean.Compiler.LCNF.PullLetDecls.Context) => { isCandidateFn := ctx.isCandidateFn, included := ∅ }) x

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

Equations

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

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

Equations

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

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

Equations

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

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 α

Equations

• x.run isCandidateFn = (x { isCandidateFn := isCandidateFn, included := ∅ }).run' { toPull := #[] }

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.pullInstances : Pass

Equations

• Lean.Compiler.LCNF.pullInstances = Lean.Compiler.LCNF.Pass.mkPerDeclaration `pullInstances Lean.Compiler.LCNF.Decl.pullInstances Lean.Compiler.LCNF.Phase.base