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
    def Lake.instInhabitedGlob.default :
    Glob
    Instances For
      source
      @[implicit_reducible]
      instance Lake.instInhabitedGlob :
      Inhabited Glob
      source
      @[implicit_reducible]
      instance Lake.instReprGlob :
      Repr Glob
      source
      def Lake.instReprGlob.repr :
      Glob → Nat → Std.Format
      Instances For
        source
        @[implicit_reducible]
        instance Lake.instDecidableEqGlob :
        DecidableEq Glob
        source
        def Lake.instDecidableEqGlob.decEq (x✝ x✝¹ : Glob) :
        Decidable (x✝ = x✝¹)
        Instances For
          source
          @[implicit_reducible]
          instance Lake.instCoeNameGlob :
          Coe Lean.Name Glob
          source
          @[implicit_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
                @[implicit_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