## Match Notation #

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

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

  Returns whether the value matches the pattern.

Instances

source
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))

Instances For

## Abstract Patterns #

source
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.

Instances For

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

- Lake.instInhabitedPattern = { default := Lake.instInhabitedPattern.default_1 }

source
def Lake.instInhabitedPattern.default_1 {a✝ : Type u_1} {a✝¹ : Type u_2} :
Pattern a✝ a✝¹
Equations

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

Instances For

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

- Lake.instInhabitedPatternDescr = { default := Lake.instInhabitedPatternDescr.default_1 }

source
def Lake.instInhabitedPatternDescr.default_1 {a✝ : Type u_1} {a✝¹ : Type u_2} :
PatternDescr a✝ a✝¹
Equations

- Lake.instInhabitedPatternDescr.default_1 = Lake.PatternDescr.not default

Instances For

source
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.

Instances For

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

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

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

Instances For

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

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

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

Instances For

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

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

source
@[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 }

Instances For

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

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

source
@[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 }

Instances For

source
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 }

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

Instances For

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

Instances For

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

Instances For

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

Matches nothing.

Equations

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

Instances For

source
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 }

Instances For

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

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

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

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

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

Matches everything.

Equations

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

Instances For

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

Matches everything.

Equations

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

Instances For

## String Patterns #

source
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.

Instances For

source
instance Lake.instInhabitedStrPatDescr :
Inhabited StrPatDescr
Equations

- Lake.instInhabitedStrPatDescr = { default := Lake.instInhabitedStrPatDescr.default }

source
def Lake.instInhabitedStrPatDescr.default :
StrPatDescr
Equations

- Lake.instInhabitedStrPatDescr.default = Lake.StrPatDescr.mem default

Instances For

source
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

Instances For

source
instance Lake.instIsPatternStrPatDescrString :
IsPattern StrPatDescr String
Equations

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

source
@[reducible, inline]
abbrev Lake.StrPat :
Type

A `String` pattern. Matches some subset of strings.

Equations

- Lake.StrPat = Lake.Pattern String Lake.StrPatDescr

Instances For

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

Matches nothing.

Equations

- Lake.StrPat.none = Lake.Pattern.empty

Instances For

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

Instances For

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

Instances For

source
instance Lake.instCoeArrayStringStrPatDescr :
Coe (Array String) StrPatDescr
Equations

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

source
instance Lake.instCoeArrayStringStrPat :
Coe (Array String) StrPat
Equations

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

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

Instances For

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

Instances For

source
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]

Instances For

source
@[inline]
def Lake.StrPat.beq (s : String) :
StrPat

Matches a string that is equal to this one.

Equations

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

Instances For

source
instance Lake.instCoeStringStrPatDescr :
Coe String StrPatDescr
Equations

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

source
instance Lake.instCoeStringStrPat :
Coe String StrPat
Equations

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

## File Path Patterns #

source
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.

Instances For

source
def Lake.instInhabitedPathPatDescr.default :
PathPatDescr
Equations

- Lake.instInhabitedPathPatDescr.default = Lake.PathPatDescr.path default

Instances For

source
instance Lake.instInhabitedPathPatDescr :
Inhabited PathPatDescr
Equations

- Lake.instInhabitedPathPatDescr = { default := Lake.instInhabitedPathPatDescr.default }

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

Instances For

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

Returns whether the file path 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

Instances For

source
instance Lake.instIsPatternPathPatDescrFilePath :
IsPattern PathPatDescr System.FilePath
Equations

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

source
@[reducible, inline]
abbrev Lake.PathPat :
Type

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

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

## Version-specific Patterns #

source
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 String.Pos.Raw.get' s 0 ⋯ == 'v' && (String.Pos.Raw.get' s { byteIdx := 1 } ⋯).isDigit else false

Instances For

source
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

Instances For

source
def Lake.defaultVersionTags :
StrPat

Default string pattern for a Package's `versionTags`.

Equations

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

Instances For

source
def Lake.versionTagPresets :
Std.TreeMap 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

Instances For