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

• isCandidateFn : Lean.Compiler.LCNF.LetDecl → Lean.FVarIdSet → Lean.Compiler.LCNF.CompilerM Bool
• included : Lean.FVarIdSet

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

• toPull : Array Lean.Compiler.LCNF.LetDecl

@[inline, reducible]

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 : Lean.FVarId) (x : Lean.Compiler.LCNF.PullLetDecls.PullM α) : Lean.Compiler.LCNF.PullLetDecls.PullM α

Equations

• Lean.Compiler.LCNF.PullLetDecls.withFVar fvarId x = withReader (fun ctx => { isCandidateFn := ctx.isCandidateFn, included := Lean.FVarIdSet.insert ctx.included fvarId }) x

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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

Equations

• Lean.Compiler.LCNF.PullLetDecls.PullM.run x isCandidateFn = StateRefT'.run' (x { isCandidateFn := isCandidateFn, included := ∅ }) { toPull := #[] }

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

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.pullInstances : Lean.Compiler.LCNF.Pass

Equations

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