@[inline]

def Lean.Compiler.LCNF.Arg.dependsOn {pu : Purity} (arg : Arg pu) (s : FVarIdSet) : Bool

Equations

• arg.dependsOn s = Lean.Compiler.LCNF.argDepOn✝ arg s

@[inline]

def Lean.Compiler.LCNF.LetValue.dependsOn {pu : Purity} (value : LetValue pu) (s : FVarIdSet) : Bool

Equations

• value.dependsOn s = Lean.Compiler.LCNF.letValueDepOn✝ value s

@[inline]

def Lean.Compiler.LCNF.LetDecl.dependsOn {pu : Purity} (decl : LetDecl pu) (s : FVarIdSet) : Bool

Equations

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

@[inline]

def Lean.Compiler.LCNF.FunDecl.dependsOn {pu : Purity} (decl : FunDecl pu) (s : 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 {pu : Purity} (decl : CodeDecl pu) (s : 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 h).dependsOn s = decl_2.dependsOn s
• (Lean.Compiler.LCNF.CodeDecl.uset fvarId i y h).dependsOn s = (Std.TreeSet.contains s fvarId || Std.TreeSet.contains s y)
• (Lean.Compiler.LCNF.CodeDecl.sset fvarId i offset y ty h).dependsOn s = (Std.TreeSet.contains s fvarId || Std.TreeSet.contains s y)
• (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h).dependsOn s = Std.TreeSet.contains s fvarId
• (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent h).dependsOn s = Std.TreeSet.contains s fvarId

def Lean.Compiler.LCNF.Code.dependsOn {pu : Purity} (c : Code pu) (s : FVarIdSet) : Bool

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

Equations

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