@[reducible, inline]

abbrev Lean.Compiler.LCNF.LetDecl.dependsOn (decl : Lean.Compiler.LCNF.LetDecl) (s : Lean.FVarIdSet) : Bool

Equations

• decl.dependsOn s = Lean.Compiler.LCNF.LetDecl.depOn✝ decl s

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FunDecl.dependsOn (decl : Lean.Compiler.LCNF.FunDecl) (s : Lean.FVarIdSet) : Bool

Equations

• decl.dependsOn s = (Lean.Compiler.LCNF.typeDepOn✝ decl.type s || Lean.Compiler.LCNF.depOn✝ decl.value s)

def Lean.Compiler.LCNF.CodeDecl.dependsOn (decl : Lean.Compiler.LCNF.CodeDecl) (s : Lean.FVarIdSet) : Bool

Equations

• (Lean.Compiler.LCNF.CodeDecl.let decl_2).dependsOn s = decl_2.dependsOn s
• (Lean.Compiler.LCNF.CodeDecl.jp decl_2).dependsOn s = decl_2.dependsOn s
• (Lean.Compiler.LCNF.CodeDecl.fun decl_2).dependsOn s = decl_2.dependsOn s

def Lean.Compiler.LCNF.Code.dependsOn (c : Lean.Compiler.LCNF.Code) (s : Lean.FVarIdSet) : Bool

Return true is c depends on a free variable in s.

Equations

• c.dependsOn s = Lean.Compiler.LCNF.depOn✝ c s