source
@[inline]
def Lean.Compiler.LCNF.LetDecl.dependsOn (decl : LetDecl) (s : FVarIdSet) :
Bool
Equations

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.FunDecl.dependsOn (decl : FunDecl) (s : FVarIdSet) :
Bool
Equations

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

Instances For

source
def Lean.Compiler.LCNF.CodeDecl.dependsOn (decl : CodeDecl) (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).dependsOn s = decl_2.dependsOn s

Instances For

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

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

Equations

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

Instances For