inductive Lake.Glob : Type

• one: Lake.Name → Lake.Glob

  Selects just the specified module name.

• submodules: Lake.Name → Lake.Glob

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

• andSubmodules: Lake.Name → Lake.Glob

  Selects the specified module and all submodules.

A specification of a set of module names.

instance Lake.instInhabitedGlob : Inhabited Lake.Glob

instance Lake.instReprGlob : Repr Lake.Glob

instance Lake.instCoeNameGlob : Coe Lake.Name Lake.Glob

partial def Lake.forEachModuleIn {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] (dir : Lake.FilePath) (f : Lake.Name → m PUnit) (ext : optParam String "lean") : m PUnit

def Lake.Glob.matches (m : Lake.Name) (self : Lake.Glob) : Bool

@[inline]

def Lake.Glob.forEachModuleIn {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] (dir : Lake.FilePath) (f : Lake.Name → m PUnit) (self : Lake.Glob) : m PUnit