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

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        Instances For
          def Lake.Glob.matches (m : Lean.Name) (self : Glob) :
          Equations
          Instances For