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

partial def Lean.Compiler.LCNF.ExtractClosed.extractLetValue (v : LetValue) : ExtractM Unit

partial def Lean.Compiler.LCNF.ExtractClosed.extractArg (arg : Arg) : ExtractM Unit

partial def Lean.Compiler.LCNF.ExtractClosed.extractFVar (fvarId : FVarId) : ExtractM Unit

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

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

• baseName : Name
• sccDecls : Array Decl

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

• decls : Array Decl

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

partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractLetValue (isRoot : Bool) (v : LetValue) : M Bool

partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractArg (arg : Arg) : M Bool

partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractFVar (fvarId : FVarId) : M Bool

partial def Lean.Compiler.LCNF.ExtractClosed.visitCode (code : Code) : M Code

def Lean.Compiler.LCNF.ExtractClosed.visitDecl (decl : Decl) : M Decl

Equations

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

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.

def Lean.Compiler.LCNF.extractClosed : Pass

Equations

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