def Regex.Matches.Spec {re : Regex} (s : re.IsSearchRegex) (haystack : String) (startPos : haystack.ValidPosPlusOne) (slice : String.Slice) (eqs : slice.str = haystack) : Prop

The slice returned by Matches functions 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

Equations

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

theorem Regex.Matches.regex_eq_of_next?_some {haystack : String} {self self' : Matches haystack} {slice : String.Slice} (h : self.next? = some (slice, self')) : self'.regex = self.regex

theorem Regex.Matches.captures_of_next?_some {haystack : String} {self self' : Matches haystack} {slice : String.Slice} (h : self.next? = some (slice, self')) (isr : self.regex.IsSearchRegex) : Spec isr haystack self.currentPos slice ⋯