def Regex.Matches.Spec {re : Regex} (s : re.IsSearchRegex) (haystack : String) (startPos : String.Pos) (str : Substring) : Prop

The pair of positions returned by Matches functions 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
• the returned substring corresponds to m.

Equations

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

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

Equations

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

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

theorem Regex.Matches.regex_eq_of_next?_some {self self' : Matches} {positions : Substring} (h : self.next? = some (positions, self')) : self'.regex = self.regex

theorem Regex.Matches.haystack_eq_of_next?_some {self self' : Matches} {positions : Substring} (h : self.next? = some (positions, self')) : self'.haystack = self.haystack

theorem Regex.Matches.vaild_matches {re : Regex} (haystack : String) (s : re.IsSearchRegex) : (re.matches haystack).Valid