Documentation

Lake.Config.Glob

inductive Lake.Glob :

A specification of a set of module names.

  • one : Lean.NameGlob

    Selects just the specified module name.

  • submodules : Lean.NameGlob

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

  • andSubmodules : Lean.NameGlob

    Selects the specified module and all submodules.

Instances For
    Equations

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

      Equations
        Instances For

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

          Equations
            Instances For
              Equations
                Instances For
                  def Lake.Glob.matches (m : Lean.Name) (self : Glob) :
                  Equations
                    Instances For
                      @[inline]
                      def Lake.Glob.forEachModuleIn {m : TypeType u_1} [Monad m] [MonadLiftT IO m] (dir : System.FilePath) (f : Lean.Namem PUnit) (self : Glob) :
                      Equations
                        Instances For