@[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.Purity.pure)) Lean.Compiler.LCNF.CompilerM

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

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

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

Equations

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

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

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.