theorem Regex.CapturedGroups.lt_of_get_some {haystack : String} {self : CapturedGroups haystack} {index : ℕ} {slice : String.Slice} (h : self.get index = some slice) : 2 * index + 1 < self.buffer.size

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

def Regex.CapturedGroups.materialize {haystack : String} (self : CapturedGroups haystack) (groups : Data.CaptureGroups haystack) : 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 : haystack.ValidPosPlusOne) (self : CapturedGroups haystack) : Prop

CapturedGroups conforms to the spec if and only if:

• The start position is valid (i.e., in the range of the haystack)
• The slice starts after the start position
• There is a regex match spanning the slice
• The captured groups contains the slices corresponding to the capture groups in the regex match
  • In particular, the first group corresponds to the slice of the overall match
  • the last match wins in case the same group is captured multiple times

Equations

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

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

theorem Regex.Captures.captures_of_next?_some {haystack : String} {self self' : Captures haystack} {captured : CapturedGroups haystack} (h : self.next? = some (captured, self')) (isr : self.regex.IsSearchRegex) : CapturedGroups.Spec isr haystack self.currentPos captured