inductive Lake.Glob : Type

A specification of a set of module names.

• one : Lean.Name → Glob

  Selects just the specified module name.

• submodules : Lean.Name → Glob

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

• andSubmodules : Lean.Name → Glob

  Selects the specified module and all submodules.

def Lake.instInhabitedGlob.default : Glob

Equations

• Lake.instInhabitedGlob.default = Lake.Glob.one default

instance Lake.instInhabitedGlob : Inhabited Glob

Equations

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

instance Lake.instReprGlob : Repr Glob

Equations

• Lake.instReprGlob = { reprPrec := Lake.instReprGlob.repr }

def Lake.instReprGlob.repr : Glob → Nat → Std.Format

Equations

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

instance Lake.instDecidableEqGlob : DecidableEq Glob

Equations

• Lake.instDecidableEqGlob = Lake.instDecidableEqGlob.decEq

def Lake.instDecidableEqGlob.decEq (x✝ x✝¹ : Glob) : Decidable (x✝ = x✝¹)

Equations

• Lake.instDecidableEqGlob.decEq (Lake.Glob.one a) (Lake.Glob.one b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.one a) (Lake.Glob.submodules a_1) = isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.one a) (Lake.Glob.andSubmodules a_1) = isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.submodules a) (Lake.Glob.one a_1) = isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.submodules a) (Lake.Glob.submodules b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.submodules a) (Lake.Glob.andSubmodules a_1) = isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.andSubmodules a) (Lake.Glob.one a_1) = isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.andSubmodules a) (Lake.Glob.submodules a_1) = isFalse ⋯
• Lake.instDecidableEqGlob.decEq (Lake.Glob.andSubmodules a) (Lake.Glob.andSubmodules b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Lake.instCoeNameGlob : Coe Lean.Name Glob

Equations

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

instance Lake.instCoeGlobArray : Coe Glob (Array 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 : 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 Glob

Equations

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

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

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 : System.FilePath) (f : Lean.Name → m PUnit) (self : Glob) : m PUnit

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 : Lean.Name) => f (a ++ x)
• Lake.Glob.forEachModuleIn dir f (Lake.Glob.andSubmodules a) = f a *> Lean.forEachModuleInDir (Lean.modToFilePath dir a "") fun (x : Lean.Name) => f (a ++ x)