@[reducible, inline]

abbrev Lean.Compiler.LCNF.UsedLocalDecls : Type

def Lean.Compiler.LCNF.collectLocalDeclsType (s : Lean.Compiler.LCNF.UsedLocalDecls) (type : Lean.Expr) : Lean.Compiler.LCNF.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.

Equations

• Lean.Compiler.LCNF.collectLocalDeclsType s type = Lean.Compiler.LCNF.collectLocalDeclsType.go s type

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

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

Equations

• Lean.Compiler.LCNF.collectLocalDeclsArg s Lean.Compiler.LCNF.Arg.erased = s
• Lean.Compiler.LCNF.collectLocalDeclsArg s (Lean.Compiler.LCNF.Arg.type e) = Lean.Compiler.LCNF.collectLocalDeclsType s e
• Lean.Compiler.LCNF.collectLocalDeclsArg s (Lean.Compiler.LCNF.Arg.fvar fvarId) = Std.HashSet.insert s fvarId

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

Equations

• Lean.Compiler.LCNF.collectLocalDeclsArgs s args = Array.foldl Lean.Compiler.LCNF.collectLocalDeclsArg s args

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

@[reducible, inline]

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

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

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

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

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

Equations

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