Documentation

Lean.Compiler.LCNF.DependsOn

source
@[inline, reducible]
abbrev Lean.Compiler.LCNF.LetDecl.dependsOn (decl : Lean.Compiler.LCNF.LetDecl) (s : Lean.FVarIdSet) :
Bool
Instances For
    source
    @[inline, reducible]
    abbrev Lean.Compiler.LCNF.FunDecl.dependsOn (decl : Lean.Compiler.LCNF.FunDecl) (s : Lean.FVarIdSet) :
    Bool
    Instances For
      source
      def Lean.Compiler.LCNF.CodeDecl.dependsOn (decl : Lean.Compiler.LCNF.CodeDecl) (s : Lean.FVarIdSet) :
      Bool
      Instances For
        source
        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.

        Instances For