Match Notation

class Lake.IsPattern (α : Type u) (β : outParam (Type v)) : Type (max u v)

• satisfies (pat : α) (val : β) : Bool

  Returns whether the value matches the pattern.

def Lake.«term_=~_» : Lean.TrailingParserDescr

Returns whether the value matches the pattern.

Equations

• Lake.«term_=~_» = Lean.ParserDescr.trailingNode `Lake.«term_=~_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =~ ") (Lean.ParserDescr.cat `term 51))

Abstract Patterns

structure Lake.Pattern (α : Type u) (β : Type v) : Type (max u v)

A pattern. Matches some subset of the values of a type. May also include a declarative description.

• filter : α → Bool

  Returns whether the value matches the pattern.

• name : Lean.Name

  An optional name for the filter.

• descr? : Option (PatternDescr α β)

  A optional declarative description of the filter.

instance Lake.instInhabitedPattern {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (Pattern a✝ a✝¹)

Equations

• Lake.instInhabitedPattern = { default := { filter := default, name := default, descr? := default } }

instance Lake.instInhabitedPatternDescr {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (PatternDescr a✝ a✝¹)

Equations

• Lake.instInhabitedPatternDescr = { default := Lake.PatternDescr.not default }

inductive Lake.PatternDescr (α : Type u) (β : Type v) : Type (max u v)

An abstract declarative pattern. Augments another pattern description β with logical connectives.

• not {α : Type u} {β : Type v} (p : Pattern α β) : PatternDescr α β

  Matches a value that does not satisfy the pattern.

• all {α : Type u} {β : Type v} (ps : Array (Pattern α β)) : PatternDescr α β

  Matches a value that satisfies every pattern. Short-circuits.

• any {α : Type u} {β : Type v} (ps : Array (Pattern α β)) : PatternDescr α β

  Matches a value that satisfies any one of the patterns. Short-circuits.

• coe {α : Type u} {β : Type v} (p : β) : PatternDescr α β

  Matches a value that statisfies the underlying pattern description.

instance Lake.instCoePatternDescr {β : Type u_1} {α : Type u_2} : Coe β (PatternDescr α β)

Equations

• Lake.instCoePatternDescr = { coe := Lake.PatternDescr.coe }

@[reducible, inline]

abbrev Lake.Pattern.matches {α : Type u_1} {β : Type u_2} (a : α) (self : Pattern α β) : Bool

Returns whether the value matches the pattern. Alias for filter.

Equations

• Lake.Pattern.matches a self = self.filter a

instance Lake.instIsPatternPattern {α : Type u_1} {β : Type u_2} : IsPattern (Pattern α β) α

Equations

• Lake.instIsPatternPattern = { satisfies := Lake.Pattern.filter }

@[specialize #[]]

def Lake.PatternDescr.matches {β : Type u_1} {α : Type u_2} [IsPattern β α] (val : α) (self : PatternDescr α β) : Bool

Returns whether the value matches the pattern.

Equations

• Lake.PatternDescr.matches val (Lake.PatternDescr.not p) = !Lake.IsPattern.satisfies p val
• Lake.PatternDescr.matches val (Lake.PatternDescr.all ps) = ps.all fun (x : Lake.Pattern α β) => Lake.IsPattern.satisfies x val
• Lake.PatternDescr.matches val (Lake.PatternDescr.any ps) = ps.any fun (x : Lake.Pattern α β) => Lake.IsPattern.satisfies x val
• Lake.PatternDescr.matches val (Lake.PatternDescr.coe p) = Lake.IsPattern.satisfies p val

instance Lake.instIsPatternPatternDescr {β : Type u_1} {α : Type u_2} [IsPattern β α] : IsPattern (PatternDescr α β) α

Equations

• Lake.instIsPatternPatternDescr = { satisfies := flip Lake.PatternDescr.matches }

@[inline]

def Lake.Pattern.ofFn {α : Type u_1} {β : Type u_2} (f : α → Bool) (name : Lean.Name := Lean.Name.anonymous) : Pattern α β

Matches a value that satisfies an arbitrary predicate (optionally identified by a Name).

Equations

• Lake.Pattern.ofFn f name = { filter := f, name := name }

instance Lake.instCoeForallBoolPattern {α : Type u_1} {β : Type u_2} : Coe (α → Bool) (Pattern α β)

Equations

• Lake.instCoeForallBoolPattern = { coe := fun (f : α → Bool) => Lake.Pattern.ofFn f }

@[inline]

def Lake.Pattern.ofDescr {β : Type (max u_1 u_2)} {α : Type u_2} [IsPattern β α] (descr : PatternDescr α β) (name : Lean.Name := Lean.Name.anonymous) : Pattern α β

Matches a string that satisfies the declarative pattern. (optionally identified by a Name).

Equations

• Lake.Pattern.ofDescr descr name = { filter := fun (x : α) => Lake.IsPattern.satisfies descr x, name := name, descr? := some descr }

instance Lake.instCoePatternDescrPatternOfIsPattern {β : Type (max u_1 u_2)} {α : Type u_1} [IsPattern β α] : Coe (PatternDescr α β) (Pattern α β)

Equations

• Lake.instCoePatternDescrPatternOfIsPattern = { coe := fun (x : Lake.PatternDescr α β) => Lake.Pattern.ofDescr x }

@[inline]

def Lake.Pattern.not {β : Type (max u_1 u_2)} {α : Type u_1} [IsPattern β α] (p : Pattern α β) : Pattern α β

Matches a value that satisfies every pattern. Short-circuits.

Equations

• p.not = Lake.Pattern.ofDescr (Lake.PatternDescr.not p)

@[inline]

def Lake.Pattern.all {β : Type (max u_1 u_2)} {α : Type u_1} [IsPattern β α] (ps : Array (Pattern α β)) : Pattern α β

Matches a value that satisfies every pattern. Short-circuits.

Equations

• Lake.Pattern.all ps = Lake.Pattern.ofDescr (Lake.PatternDescr.all ps)

@[inline]

def Lake.Pattern.any {β : Type (max u_1 u_2)} {α : Type u_1} [IsPattern β α] (ps : Array (Pattern α β)) : Pattern α β

Matches a value that satisfies every pattern. Short-circuits.

Equations

• Lake.Pattern.any ps = Lake.Pattern.ofDescr (Lake.PatternDescr.any ps)

def Lake.PatternDescr.empty {α : Type u_1} {β : Type u_2} : PatternDescr α β

Matches nothing.

Equations

• Lake.PatternDescr.empty = Lake.PatternDescr.any #[]

def Lake.Pattern.empty {α : Type u_1} {β : Type u_2} : Pattern α β

Matches nothing.

Equations

• Lake.Pattern.empty = { filter := fun (x : α) => false, name := `empty, descr? := some Lake.PatternDescr.empty }

instance Lake.instEmptyCollectionPatternDescr {α : Type u_1} {β : Type u_2} : EmptyCollection (PatternDescr α β)

Equations

• Lake.instEmptyCollectionPatternDescr = { emptyCollection := Lake.PatternDescr.empty }

instance Lake.instEmptyCollectionPattern {α : Type u_1} {β : Type u_2} : EmptyCollection (Pattern α β)

Equations

• Lake.instEmptyCollectionPattern = { emptyCollection := Lake.Pattern.empty }

def Lake.PatternDescr.star {α : Type u_1} {β : Type u_2} : PatternDescr α β

Matches eveything.

Equations

• Lake.PatternDescr.star = Lake.PatternDescr.all #[]

def Lake.Pattern.star {α : Type u_1} {β : Type u_2} : Pattern α β

Matches eveything.

Equations

• Lake.Pattern.star = { filter := fun (x : α) => true, name := `star, descr? := some Lake.PatternDescr.star }

String Patterns

inductive Lake.StrPatDescr : Type

A declarative String pattern. Matches some subset of strings.

• mem (xs : Array String) : StrPatDescr

  Matches a string that is a member of the array

• startsWith (affix : String) : StrPatDescr

  Matches a string that starts with this prefix.

• endsWith (affix : String) : StrPatDescr

  Matches a string that ends with this suffix.

instance Lake.instInhabitedStrPatDescr : Inhabited StrPatDescr

Equations

• Lake.instInhabitedStrPatDescr = { default := Lake.StrPatDescr.mem default }

def Lake.StrPatDescr.matches (s : String) (self : StrPatDescr) : Bool

Returns whether the string matches the pattern.

Equations

• Lake.StrPatDescr.matches s (Lake.StrPatDescr.mem xs) = xs.contains s
• Lake.StrPatDescr.matches s (Lake.StrPatDescr.startsWith x) = s.startsWith x
• Lake.StrPatDescr.matches s (Lake.StrPatDescr.endsWith x) = s.endsWith x

instance Lake.instIsPatternStrPatDescrString : IsPattern StrPatDescr String

Equations

• Lake.instIsPatternStrPatDescrString = { satisfies := flip Lake.StrPatDescr.matches }

@[reducible, inline]

abbrev Lake.StrPat : Type

A String pattern. Matches some subset of strings.

Equations

• Lake.StrPat = Lake.Pattern String Lake.StrPatDescr

@[reducible, inline, deprecated Lake.Pattern.empty (since := "2025-03-27")]

abbrev Lake.StrPat.none : StrPat

Matches nothing.

Equations

• Lake.StrPat.none = Lake.Pattern.empty

@[reducible, inline, deprecated Lake.Pattern.ofFn (since := "2025-03-27")]

abbrev Lake.StrPat.satisfies (f : String → Bool) (name : Lean.Name := Lean.Name.anonymous) : StrPat

Matches a value that satisfies an arbitrary predicate (optionally identified by a Name).

Equations

• Lake.StrPat.satisfies f name = Lake.Pattern.ofFn f name

@[inline]

def Lake.StrPat.mem (xs : Array String) : StrPat

Matches a string that is a member of the array

Equations

• Lake.StrPat.mem xs = Lake.Pattern.ofDescr (Lake.PatternDescr.coe (Lake.StrPatDescr.mem xs))

instance Lake.instCoeArrayStringStrPatDescr : Coe (Array String) StrPatDescr

Equations

• Lake.instCoeArrayStringStrPatDescr = { coe := Lake.StrPatDescr.mem }

instance Lake.instCoeArrayStringStrPat : Coe (Array String) StrPat

Equations

• Lake.instCoeArrayStringStrPat = { coe := Lake.StrPat.mem }

@[inline]

def Lake.StrPat.startsWith (affix : String) : StrPat

Matches a string that starts with this prefix.

Equations

• Lake.StrPat.startsWith affix = Lake.Pattern.ofDescr (Lake.PatternDescr.coe (Lake.StrPatDescr.startsWith affix))

@[inline]

def Lake.StrPat.endsWith (affix : String) : StrPat

Matches a string that ends with this suffix.

Equations

• Lake.StrPat.endsWith affix = Lake.Pattern.ofDescr (Lake.PatternDescr.coe (Lake.StrPatDescr.endsWith affix))

def Lake.StrPatDescr.beq (s : String) : StrPatDescr

Matches a string that is equal to this one.

Equations

• Lake.StrPatDescr.beq s = Lake.StrPatDescr.mem #[s]

@[inline]

def Lake.StrPat.beq (s : String) : StrPat

Matches a string that is a member of the array

Equations

• Lake.StrPat.beq s = { filter := fun (x : String) => x == s, descr? := some (Lake.PatternDescr.coe (Lake.StrPatDescr.beq s)) }

instance Lake.instCoeStringStrPatDescr : Coe String StrPatDescr

Equations

• Lake.instCoeStringStrPatDescr = { coe := Lake.StrPatDescr.beq }

instance Lake.instCoeStringStrPat : Coe String StrPat

Equations

• Lake.instCoeStringStrPat = { coe := Lake.StrPat.beq }

File Path Patterns

inductive Lake.PathPatDescr : Type

A declarative FilePath pattern. Matches some subset of file paths.

• path (p : StrPat) : PathPatDescr

  Matches a file path whose normalized string representation satisfies the pattern.

• extension (p : StrPat) : PathPatDescr

  Matches a file path whose extension satisfies the pattern.

• fileName (p : StrPat) : PathPatDescr

  Matches a file path whose name satisfies the pattern.

instance Lake.instInhabitedPathPatDescr : Inhabited PathPatDescr

Equations

• Lake.instInhabitedPathPatDescr = { default := Lake.PathPatDescr.path default }

@[inline]

def Lake.PathPatDescr.eq (p : System.FilePath) : PathPatDescr

Matches a file path that is equal to this one (when both are normalized).

Equations

• Lake.PathPatDescr.eq p = Lake.PathPatDescr.path (Lake.StrPat.beq p.toString)

def Lake.PathPatDescr.matches (path : System.FilePath) (self : PathPatDescr) : Bool

Returns whether the string matches the pattern.

Equations

• Lake.PathPatDescr.matches path (Lake.PathPatDescr.path p) = Lake.IsPattern.satisfies p path.normalize.toString
• Lake.PathPatDescr.matches path (Lake.PathPatDescr.extension p) = Option.any (fun (x : String) => Lake.IsPattern.satisfies p x) path.extension
• Lake.PathPatDescr.matches path (Lake.PathPatDescr.fileName p) = Option.any (fun (x : String) => Lake.IsPattern.satisfies p x) path.fileName

instance Lake.instIsPatternPathPatDescrFilePath : IsPattern PathPatDescr System.FilePath

Equations

• Lake.instIsPatternPathPatDescrFilePath = { satisfies := flip Lake.PathPatDescr.matches }

@[reducible, inline]

abbrev Lake.PathPat : Type

A FilePath pattern. Matches some subset of file paths.

Equations

• Lake.PathPat = Lake.Pattern System.FilePath Lake.PathPatDescr

@[inline]

def Lake.PathPat.path (p : StrPat) : PathPat

Matches a file path whose normalized string representation satisfies the pattern.

Equations

• Lake.PathPat.path p = Lake.Pattern.ofDescr (Lake.PatternDescr.coe (Lake.PathPatDescr.path p))

@[inline]

def Lake.PathPat.extension (p : StrPat) : PathPat

Matches a file path whose extension satisfies the pattern.

Equations

• Lake.PathPat.extension p = Lake.Pattern.ofDescr (Lake.PatternDescr.coe (Lake.PathPatDescr.extension p))

@[inline]

def Lake.PathPat.fileName (p : StrPat) : PathPat

Matches a file path whose name satisfies the pattern.

Equations

• Lake.PathPat.fileName p = Lake.Pattern.ofDescr (Lake.PatternDescr.coe (Lake.PathPatDescr.fileName p))

Version-specific Patterns

def Lake.isVerLike (s : String) : Bool

Whether a string is "version-like". That is, a v followed by a digit.

Equations

• Lake.isVerLike s = if h : s.utf8ByteSize ≥ 2 then s.get' 0 ⋯ == 'v' && (s.get' { byteIdx := 1 } ⋯).isDigit else false

def Lake.StrPat.verLike : StrPat

Matches a "version-like" string: a v followed by a digit.

Equations

• Lake.StrPat.verLike = Lake.Pattern.ofFn Lake.isVerLike `verLike

def Lake.defaultVersionTags : StrPat

Default string pattern for a Package's versionTags.

Equations

• Lake.defaultVersionTags = Lake.Pattern.ofFn Lake.isVerLike `default

def Lake.versionTagPresets : Lean.RBMap Lean.Name StrPat Lean.Name.quickCmp

Builtin StrPat presets available to TOML for versionTags.

Equations

• Lake.versionTagPresets = (Lake.NameMap.empty.insert `verLike Lake.StrPat.verLike).insert `default Lake.defaultVersionTags