structure Regex.CapturedGroups (haystack : String) : Type

A structure representing the capture groups from a regex match.

Contains the original string (haystack) and a buffer of positions marking the start and end of each capture group.

• buffer : Array haystack.ValidPosPlusOne

instance Regex.instReprCapturedGroups {haystack✝ : String} : Repr (CapturedGroups haystack✝)

Equations

• Regex.instReprCapturedGroups = { reprPrec := Regex.instReprCapturedGroups.repr }

def Regex.instReprCapturedGroups.repr {haystack✝ : String} : CapturedGroups haystack✝ → Nat → Std.Format

Equations

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

def Regex.instDecidableEqCapturedGroups.decEq {haystack✝ : String} (x✝ x✝¹ : CapturedGroups haystack✝) : Decidable (x✝ = x✝¹)

Equations

• Regex.instDecidableEqCapturedGroups.decEq { buffer := a } { buffer := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Regex.instDecidableEqCapturedGroups {haystack✝ : String} : DecidableEq (CapturedGroups haystack✝)

Equations

• Regex.instDecidableEqCapturedGroups = Regex.instDecidableEqCapturedGroups.decEq

def Regex.instInhabitedCapturedGroups.default {a✝ : String} : CapturedGroups a✝

Equations

• Regex.instInhabitedCapturedGroups.default = { buffer := default }

instance Regex.instInhabitedCapturedGroups {a✝ : String} : Inhabited (CapturedGroups a✝)

Equations

• Regex.instInhabitedCapturedGroups = { default := Regex.instInhabitedCapturedGroups.default }

def Regex.CapturedGroups.get {haystack : String} (self : CapturedGroups haystack) (index : Nat) : Option String.Slice

Gets a specific capture group as a substring.

• self: The captured groups
• index: The index of the capture group to retrieve (0 for the entire match)
• Returns: An optional substring representing the capture group, or none if the group didn't participate in the match

Equations

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

theorem Regex.CapturedGroups.get_str_eq_some {haystack : String} {self : CapturedGroups haystack} {index : Nat} {s : String.Slice} (h : self.get index = some s) : s.str = haystack

def Regex.CapturedGroups.toArray {haystack : String} (self : CapturedGroups haystack) : Array (Option String.Slice)

Converts all capture groups to an array of optional substrings.

• self: The captured groups
• Returns: An array where each element is either a substring for a capture group or none if that group didn't participate in the match

Equations

• self.toArray = Regex.CapturedGroups.toArray.go self 0 #[]

@[irreducible]

def Regex.CapturedGroups.toArray.go {haystack : String} (self : CapturedGroups haystack) (i : Nat) (accum : Array (Option String.Slice)) : Array (Option String.Slice)

Equations

• Regex.CapturedGroups.toArray.go self i accum = if 2 * i < self.buffer.size then Regex.CapturedGroups.toArray.go self (i + 1) (accum.push (self.get i)) else accum

structure Regex.Captures (haystack : String) : Type

A structure that enables iterating through all capture groups of regex matches in a string.

Provides a stateful iterator for finding all regex matches and their capture groups in a haystack string.

• regex : Regex
• currentPos : haystack.ValidPosPlusOne

instance Regex.instReprCaptures {haystack✝ : String} : Repr (Captures haystack✝)

Equations

• Regex.instReprCaptures = { reprPrec := Regex.instReprCaptures.repr }

def Regex.instReprCaptures.repr {haystack✝ : String} : Captures haystack✝ → Nat → Std.Format

Equations

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

def Regex.Captures.next? {haystack : String} (self : Captures haystack) : Option (CapturedGroups haystack × Captures haystack)

Gets the next match and its capture groups.

• self: The captures iterator
• Returns: An optional pair containing the captured groups and an updated iterator, or none if no more matches are found

Equations

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

theorem Regex.Captures.zeroth_group_some_of_next?_some {haystack : String} {self next : Captures haystack} {groups : CapturedGroups haystack} (h : self.next? = some (groups, next)) : (groups.get 0).isSome = true

theorem Regex.Captures.lt_next?_some' {haystack : String} {groups : CapturedGroups haystack} {c c' : Captures haystack} (h : c.next? = some (groups, c')) : c.currentPos < c'.currentPos

def Regex.Captures.lt {haystack : String} (c c' : Captures haystack) : Prop

Equations

• c.lt c' = (c.currentPos < c'.currentPos)

instance Regex.Captures.instLT {haystack : String} : LT (Captures haystack)

Equations

• Regex.Captures.instLT = { lt := Regex.Captures.lt }

@[simp]

theorem Regex.Captures.lt_next?_some {haystack : String} {groups : CapturedGroups haystack} {c c' : Captures haystack} (h : c.next? = some (groups, c')) : c < c'

theorem Regex.Captures.wellFounded_gt {haystack : String} : WellFounded fun (p q : Captures haystack) => q < p

instance Regex.Captures.instWellFoundedRelation {haystack : String} : WellFoundedRelation (Captures haystack)

Equations

• Regex.Captures.instWellFoundedRelation = { rel := fun (p q : Regex.Captures haystack) => q < p, wf := ⋯ }

instance Regex.Captures.instStreamCapturedGroups {haystack : String} : Std.Stream (Captures haystack) (CapturedGroups haystack)

Equations

• Regex.Captures.instStreamCapturedGroups = { next? := Regex.Captures.next? }

def Regex.captures (regex : Regex) (s : String) : Captures s

Creates a new Captures iterator for a regex pattern and input string.

• regex: The compiled regex pattern to use for matching
• s: The input string to search in
• Returns: A Captures iterator positioned at the start of the string

Equations

• regex.captures s = { regex := regex, currentPos := s.startValidPosPlusOne }