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

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 Purity.pure)) (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 }) x

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

Equations

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

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

Equations

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

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

Equations

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

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 α

Equations

• x.run isCandidateFn = (x { isCandidateFn := isCandidateFn }).run' { }

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

Equations

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

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

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.Phase.base Lean.Compiler.LCNF.Decl.pullInstances