@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Compiler.LCNF.FunDecl.dependsOn decl 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

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

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

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