Documentation

Lean.Compiler.LCNF.DependsOn

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