@[reducible, inline]

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

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

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

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

def Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (arg : Arg Purity.pure) : Bool

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

• baseName : Name
• sccDecls : Array (Decl Purity.pure)

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

• decls : Array (Decl Purity.pure)
• 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 Purity.pure) : M Bool

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

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

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

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

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

def Lean.Compiler.LCNF.extractClosed : Pass