@[reducible, inline]

abbrev Lean.Compiler.LCNF.ExtractClosed.ExtractM (α : Type) : Type

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

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

• baseName : Name
• sccDecls : Array Decl

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

• decls : Array Decl
• fvarDecisionCache : Std.HashMap FVarId Bool

  Cache for shouldExtractFVar in order to avoid superlinear behavior.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.ExtractClosed.M (α : Type) : Type

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

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

def Lean.Compiler.LCNF.extractClosed : Pass