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.

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✝¹)

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

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 satisfies the underlying pattern description.

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

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

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

@[specialize #[]]

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

Returns whether the value matches the pattern.

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

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

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

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

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

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

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

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

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

Matches nothing.

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

Matches nothing.

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

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

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

Matches everything.

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

Matches everything.

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

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

Returns whether the string matches the pattern.

instance Lake.instIsPatternStrPatDescrString : IsPattern StrPatDescr String

@[reducible, inline]

abbrev Lake.StrPat : Type

A String pattern. Matches some subset of strings.

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

abbrev Lake.StrPat.none : StrPat

Matches nothing.

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

@[inline]

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

Matches a string that is a member of the array

instance Lake.instCoeArrayStringStrPatDescr : Coe (Array String) StrPatDescr

instance Lake.instCoeArrayStringStrPat : Coe (Array String) StrPat

@[inline]

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

Matches a string that starts with this prefix.

@[inline]

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

Matches a string that ends with this suffix.

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

Matches a string that is equal to this one.

@[inline]

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

Matches a string that is a member of the array

instance Lake.instCoeStringStrPatDescr : Coe String StrPatDescr

instance Lake.instCoeStringStrPat : Coe String StrPat

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

@[inline]

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

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

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

Returns whether the string matches the pattern.

instance Lake.instIsPatternPathPatDescrFilePath : IsPattern PathPatDescr System.FilePath

@[reducible, inline]

abbrev Lake.PathPat : Type

A FilePath pattern. Matches some subset of file paths.

@[inline]

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

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

@[inline]

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

Matches a file path whose extension satisfies the pattern.

@[inline]

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

Matches a file path whose name satisfies the pattern.

Version-specific Patterns

def Lake.isVerLike (s : String) : Bool

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

def Lake.StrPat.verLike : StrPat

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

def Lake.defaultVersionTags : StrPat

Default string pattern for a Package's versionTags.

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

Builtin StrPat presets available to TOML for versionTags.