Documentation

Lake.Config.Glob

source
inductive Lake.Glob :
Type

A specification of a set of module names.

  • one : Lean.Name → Glob

    Selects just the specified module name.

  • submodules : Lean.Name → Glob

    Selects all submodules of the specified module, but not the module itself.

  • andSubmodules : Lean.Name → Glob

    Selects the specified module and all submodules.

Instances For
    source
    @[instance_reducible]
    instance Lake.instInhabitedGlob :
    Inhabited Glob
    source
    @[instance_reducible]
    instance Lake.instReprGlob :
    Repr Glob
    source
    def Lake.instReprGlob.repr :
    Glob → Nat → Std.Format
    Instances For
      source
      def Lake.instDecidableEqGlob.decEq (x✝ x✝¹ : Glob) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance Lake.instDecidableEqGlob :
        DecidableEq Glob
        source
        @[instance_reducible]
        instance Lake.instCoeNameGlob :
        Coe Lean.Name Glob
        source
        @[instance_reducible]
        instance Lake.instCoeGlobArray :
        Coe Glob (Array Glob)
        source
        def Lake.«term__.*» :
        Lean.ParserDescr

        A name glob which matches all names with the prefix, including itself.

        Instances For
          source
          def Lake.«term__.+» :
          Lean.ParserDescr

          A name glob which matches all names with the prefix, but not the prefix itself.

          Instances For
            source
            def Lake.Glob.toString :
            Glob → String
            Instances For
              source
              @[instance_reducible]
              instance Lake.Glob.instToString :
              ToString Glob
              source
              def Lake.Glob.matches (m : Lean.Name) (self : Glob) :
              Bool
              Instances For
                source
                @[inline]
                def Lake.Glob.forEachModuleIn {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] (dir : System.FilePath) (f : Lean.Name → m PUnit) (self : Glob) :
                m PUnit
                Instances For