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

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

Instances For

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

- toPull : Array LetDecl

Instances For

source
@[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)

Instances For

source
@[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.

Instances For

source
@[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.

Instances For

source
@[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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
partial def Lean.Compiler.LCNF.PullLetDecls.pullAlt (alt : Alt) :
PullM Alt
source
partial def Lean.Compiler.LCNF.PullLetDecls.pullDecls (code : Code) :
PullM Code
source
def Lean.Compiler.LCNF.PullLetDecls.PullM.run {α : Type} (x : PullM α) (isCandidateFn : LetDecl → FVarIdSet → CompilerM Bool) :
CompilerM α
Equations

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

Instances For

source
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.

Instances For

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

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

Instances For

source
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

Instances For