Documentation

Lake.Config.Glob

inductive Lake.Glob :

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

instance Lake.instInhabitedGlob :

Inhabited Lake.Glob

Equations

Lake.instInhabitedGlob = { default := Lake.Glob.one default }

instance Lake.instReprGlob :

Equations

Lake.instReprGlob = { reprPrec := Lake.reprGlob✝ }

instance Lake.instDecidableEqGlob :

DecidableEq Lake.Glob

Equations

Lake.instDecidableEqGlob = Lake.decEqGlob✝

instance Lake.instCoeNameGlob :

Coe Lake.Name Lake.Glob

Equations

Lake.instCoeNameGlob = { coe := Lake.Glob.one }

instance Lake.instCoeGlobArray :

Coe Lake.Glob (Array Lake.Glob)

Equations

Lake.instCoeGlobArray = { coe := Array.singleton }

def Lake.«term__.*» :

Lean.ParserDescr

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.

def Lake.«term__.+» :

Lean.ParserDescr

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.

def Lake.Glob.toString :

Lake.Glob → String

Equations

(Lake.Glob.one a).toString = a.toString
(Lake.Glob.submodules a).toString = a.toString ++ ".+"
(Lake.Glob.andSubmodules a).toString = a.toString ++ ".*"

instance Lake.Glob.instToString :

ToString Lake.Glob

Equations

Lake.Glob.instToString = { toString := Lake.Glob.toString }

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

Equations

Lake.Glob.matches m (Lake.Glob.one a) = (a == m)
Lake.Glob.matches m (Lake.Glob.submodules a) = (a.isPrefixOf m && a != m)
Lake.Glob.matches m (Lake.Glob.andSubmodules a) = a.isPrefixOf m

@[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) :

Equations

Lake.Glob.forEachModuleIn dir f (Lake.Glob.one a) = f a
Lake.Glob.forEachModuleIn dir f (Lake.Glob.submodules a) = Lean.forEachModuleInDir (Lean.modToFilePath dir a "") fun (x : Lake.Name) => f (a ++ x)
Lake.Glob.forEachModuleIn dir f (Lake.Glob.andSubmodules a) = SeqRight.seqRight (f a) fun (x : Unit) => Lean.forEachModuleInDir (Lean.modToFilePath dir a "") fun (x : Lake.Name) => f (a ++ x)