@[inline]

abbrev Lean.Compiler.LCNF.UsedLocalDecls : Type

Equations

• Lean.Compiler.LCNF.UsedLocalDecls = Lean.FVarIdHashSet

def Lean.Compiler.LCNF.collectLocalDecls (s : Lean.Compiler.LCNF.UsedLocalDecls) (e : 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.collectLocalDecls s e = Lean.Compiler.LCNF.collectLocalDecls.go s e

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.collectLocalDecls.go s (Lean.Expr.proj typeName idx e_2) = Lean.Compiler.LCNF.collectLocalDecls.go s e_2
• Lean.Compiler.LCNF.collectLocalDecls.go s (Lean.Expr.forallE binderName binderType body binderInfo) = s
• Lean.Compiler.LCNF.collectLocalDecls.go s (Lean.Expr.lam binderName binderType b binderInfo) = Lean.Compiler.LCNF.collectLocalDecls.go s b
• Lean.Compiler.LCNF.collectLocalDecls.go s (Lean.Expr.app f a) = Lean.Compiler.LCNF.collectLocalDecls.go (Lean.Compiler.LCNF.collectLocalDecls.go s a) f
• Lean.Compiler.LCNF.collectLocalDecls.go s (Lean.Expr.mdata data b) = Lean.Compiler.LCNF.collectLocalDecls.go s b
• Lean.Compiler.LCNF.collectLocalDecls.go s (Lean.Expr.fvar fvarId) = Lean.HashSet.insert s fvarId
• Lean.Compiler.LCNF.collectLocalDecls.go s e = s

@[inline]

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

Equations

• Lean.Compiler.LCNF.ElimDead.M = StateRefT' IO.RealWorld Lean.Compiler.LCNF.UsedLocalDecls Lean.Compiler.LCNF.CompilerM

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

Equations

• Lean.Compiler.LCNF.Code.elimDead code = StateRefT'.run' (Lean.Compiler.LCNF.ElimDead.elimDead 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.