inductive Lake.Glob : Type

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.

instance Lake.instInhabitedGlob : Inhabited Lake.Glob

Equations

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

instance Lake.instReprGlob : Repr Lake.Glob

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

• x.toString = match x with | Lake.Glob.one n => n.toString | Lake.Glob.submodules n => n.toString ++ ".+" | Lake.Glob.andSubmodules n => n.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) : Bool

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

@[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.