theorem Regex.Data.BVPos.ext_index {s : String} {startPos : s.ValidPos} {p₁ p₂ : BVPos startPos} (h₂ : p₁.index = p₂.index) : p₁ = p₂

theorem Regex.Data.BVPos.ext_index_iff {s : String} {startPos : s.ValidPos} {p₁ p₂ : BVPos startPos} : p₁ = p₂ ↔ p₁.index = p₂.index

def Regex.Data.BVPos.Splits {s : String} {startPos : s.ValidPos} (p : BVPos startPos) (l r : String) : Prop

Equations

• p.Splits l r = p.current.Splits l r