source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ExtractClosed.ExtractM (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.ExtractClosed.ExtractM = StateRefT' IO.RealWorld (Array Lean.Compiler.LCNF.CodeDecl) Lean.Compiler.LCNF.CompilerM

Instances For

source
partial def Lean.Compiler.LCNF.ExtractClosed.extractLetValue (v : LetValue) :
ExtractM Unit
source
partial def Lean.Compiler.LCNF.ExtractClosed.extractArg (arg : Arg) :
ExtractM Unit
source
partial def Lean.Compiler.LCNF.ExtractClosed.extractFVar (fvarId : FVarId) :
ExtractM Unit
source
def Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (arg : Arg) :
Bool
Equations

- Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg Lean.Compiler.LCNF.Arg.erased = true
- Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (Lean.Compiler.LCNF.Arg.type expr) = true
- Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = false

Instances For

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

- baseName : Name
- sccDecls : Array Decl

Instances For

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

- decls : Array Decl

Instances For

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ExtractClosed.M (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.ExtractClosed.M = ReaderT Lean.Compiler.LCNF.ExtractClosed.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.ExtractClosed.State Lean.Compiler.LCNF.CompilerM)

Instances For

source
partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractLetValue (isRoot : Bool) (v : LetValue) :
M Bool
source
partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractArg (arg : Arg) :
M Bool
source
partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractFVar (fvarId : FVarId) :
M Bool
source
partial def Lean.Compiler.LCNF.ExtractClosed.visitCode (code : Code) :
M Code
source
def Lean.Compiler.LCNF.ExtractClosed.visitDecl (decl : Decl) :
M Decl
Equations

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

Instances For

source
def Lean.Compiler.LCNF.Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) :
CompilerM (Array Decl)
Equations

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

Instances For

source
def Lean.Compiler.LCNF.extractClosed :
Pass
Equations

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

Instances For