@[reducible, inline]

abbrev Lean.Compiler.LCNF.UsedLocalDecls : Type

def Lean.Compiler.LCNF.collectLocalDeclsType (s : UsedLocalDecls) (type : Expr) : UsedLocalDecls

Collect set of (let) free variables in a LCNF value. This code exploits the LCNF property that local declarations do not occur in types.

def Lean.Compiler.LCNF.collectLocalDeclsType.go (s : UsedLocalDecls) (e : Expr) : UsedLocalDecls

def Lean.Compiler.LCNF.collectLocalDeclsArg (s : UsedLocalDecls) (arg : Arg) : UsedLocalDecls

def Lean.Compiler.LCNF.collectLocalDeclsArgs (s : UsedLocalDecls) (args : Array Arg) : UsedLocalDecls

def Lean.Compiler.LCNF.collectLocalDeclsLetValue (s : UsedLocalDecls) (e : LetValue) : UsedLocalDecls

@[reducible, inline]

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

partial def Lean.Compiler.LCNF.ElimDead.visitFunDecl (funDecl : FunDecl) : M FunDecl

partial def Lean.Compiler.LCNF.ElimDead.elimDead (code : Code) : M Code

def Lean.Compiler.LCNF.Code.elimDead (code : Code) : CompilerM Code

def Lean.Compiler.LCNF.Decl.elimDead (decl : Decl) : CompilerM Decl