Documentation

Lean.Compiler.LCNF.DependsOn

source
@[inline]
def Lean.Compiler.LCNF.Arg.dependsOn {pu : Purity} (arg : Arg pu) (s : FVarIdSet) :
Bool
Instances For
    source
    @[inline]
    def Lean.Compiler.LCNF.LetValue.dependsOn {pu : Purity} (value : LetValue pu) (s : FVarIdSet) :
    Bool
    Instances For
      source
      @[inline]
      def Lean.Compiler.LCNF.LetDecl.dependsOn {pu : Purity} (decl : LetDecl pu) (s : FVarIdSet) :
      Bool
      Instances For
        source
        @[inline]
        def Lean.Compiler.LCNF.FunDecl.dependsOn {pu : Purity} (decl : FunDecl pu) (s : FVarIdSet) :
        Bool
        Instances For
          source
          def Lean.Compiler.LCNF.CodeDecl.dependsOn {pu : Purity} (decl : CodeDecl pu) (s : FVarIdSet) :
          Bool
          Instances For
            source
            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.

            Instances For