A specification of a set of module names.
- 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.
Instances For
Equations
- Lake.instInhabitedGlob = { default := Lake.Glob.one default }
Equations
- Lake.instReprGlob = { reprPrec := Lake.reprGlob✝ }
Equations
Equations
- Lake.instCoeNameGlob = { coe := Lake.Glob.one }
Equations
- Lake.instCoeGlobArray = { coe := Array.singleton }
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
- x.toString = match x with | Lake.Glob.one n => n.toString | Lake.Glob.submodules n => n.toString ++ ".+" | Lake.Glob.andSubmodules n => n.toString ++ ".*"
Instances For
Equations
- Lake.Glob.instToString = { toString := Lake.Glob.toString }
Equations
- Lake.Glob.matches m x = match x with | Lake.Glob.one n => n == m | Lake.Glob.submodules n => n.isPrefixOf m && n != m | Lake.Glob.andSubmodules n => n.isPrefixOf m
Instances For
@[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
Equations
- One or more equations did not get rendered due to their size.