Regex

Definitions for Regex api

@[reducible, inline]

abbrev Regex.ValidSubstring : Type

Equations

• Regex.ValidSubstring = { s : Substring // s.Valid }

@[reducible, inline]

abbrev Regex.ValidPos (s : String) : Type

Equations

• Regex.ValidPos s = { pos : String.Pos // String.Pos.Valid s pos }

instance Regex.instSubstringValid (s : ValidSubstring) : Inhabited (ValidPos s.val.str)

Equations

• Regex.instSubstringValid s = { default := ⟨s.val.startPos, ⋯⟩ }

instance Regex.instCoeStringValidSubstring : Coe String ValidSubstring

Equations

• Regex.instCoeStringValidSubstring = { coe := fun (s : String) => ⟨s.toSubstring, ⋯⟩ }

@[reducible, inline]

abbrev Regex.Match : Type

Represents a single match of a regex in a haystack.

Equations

• Regex.Match = Regex.ValidSubstring

instance Regex.instToStringMatch : ToString Match

Equations

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

structure Regex.Captures (s : String) : Type

Represents the full match and capture groups for a single match in s.

• fullMatch : Match

  the full match

• groups : Array (Option Match)

  the capture groups, empty groups can arise, for example, in alternatives

• isSubstringOf : self.fullMatch.val.str = s

  fullMatch is a substring of s.

• areSubstringsOf : (self.groups.all fun (x : Option Match) => Option.all (fun (x : Match) => decide (x.val.str = s)) x) = true

  all matches in groups are substrings of s.

theorem Regex.start_pos_valid_of {s : ValidSubstring} (captures : Captures s.val.str) : String.Pos.Valid s.val.str captures.fullMatch.val.startPos

theorem Regex.stop_pos_valid_of {s : ValidSubstring} (captures : Captures s.val.str) : String.Pos.Valid s.val.str captures.fullMatch.val.stopPos