theorem Regex.CapturedGroups.lt_of_get_some {self : CapturedGroups} {i : ℕ} {s : Substring} (h : self.get i = some s) : 2 * i + 1 < self.buffer.size

theorem Regex.CapturedGroups.get_eq_none_of_ge {self : CapturedGroups} {i : ℕ} (h : 2 * i + 1 ≥ self.buffer.size) : self.get i = none

def Regex.CapturedGroups.materialize (self : CapturedGroups) (groups : Data.CaptureGroups) : Prop

Equations

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

def Regex.CapturedGroups.Spec {re : Regex} (s : re.IsSearchRegex) (haystack : String) (startPos : String.Pos) (self : CapturedGroups) : Prop

CapturedGroups conforms to the spec if and only if:

• the haystack can be split into l, m, and r such that haystack = l ++ m ++ r
• m starts after startPos.
• there is a regex match starting at l, matching the substring m, and ending at r
• CapturedGroups contains the positions of the capture groups in the match
  • in particular, the first group corresponds to the positions of the matched substring m
  • the last match of wins in case the same group is captured multiple times

Equations

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

def Regex.Captures.Valid (self : Captures) : Prop

Equations

• self.Valid = (self.regex.IsSearchRegex ∧ String.Pos.ValidPlus self.haystack self.currentPos)

theorem Regex.Captures.captures_of_next?_some {self self' : Captures} {captured : CapturedGroups} (h : self.next? = some (captured, self')) (v : self.Valid) : self'.Valid ∧ CapturedGroups.Spec ⋯ self.haystack self.currentPos captured

theorem Regex.Captures.regex_eq_of_next?_some {self self' : Captures} {captured : CapturedGroups} (h : self.next? = some (captured, self')) : self'.regex = self.regex

theorem Regex.Captures.haystack_eq_of_next?_some {self self' : Captures} {captured : CapturedGroups} (h : self.next? = some (captured, self')) : self'.haystack = self.haystack

theorem Regex.Captures.valid_captures {re : Regex} (haystack : String) (s : re.IsSearchRegex) : (re.captures haystack).Valid