theorem String.Pos.valid_of_isValidAux (cs : List Char) (p i : Pos) (h : isValid.go p cs i = true) : ∃ (cs₁ : List Char), ∃ (cs₂ : List Char), cs = cs₁ ++ cs₂ ∧ p = i + { byteIdx := utf8Len cs₁ }

theorem String.Pos.valid_of_isValid {s : String} {p : Pos} (v : isValid s p = true) : Valid s p

theorem String.Pos.isValid_of_validAux (cs₁ cs₂ : List Char) (p i : Pos) (hp : p = i + { byteIdx := utf8Len cs₁ }) : isValid.go p (cs₁ ++ cs₂) i = true

theorem String.Pos.isValid_of_valid (cs₁ cs₂ : List Char) (p : Pos) (hp : p = { byteIdx := utf8Len cs₁ }) : isValid { data := cs₁ ++ cs₂ } p = true

theorem String.Iterator.ext {it₁ it₂ : Iterator} (hs : it₁.s = it₂.s) (hi : it₁.i = it₂.i) : it₁ = it₂

theorem String.Iterator.ext_iff {it₁ it₂ : Iterator} : it₁ = it₂ ↔ it₁.s = it₂.s ∧ it₁.i = it₂.i

theorem String.Iterator.hasNext_of_not_atEnd {it : Iterator} (h : ¬it.atEnd = true) : it.hasNext = true

@[simp]

theorem String.Iterator.ne_next (it : Iterator) : it ≠ it.next

@[simp]

theorem String.Iterator.next_ne (it : Iterator) : it.next ≠ it

theorem String.Iterator.nextn_next_eq_next_nextn (it : Iterator) (n : ℕ) : (it.nextn n).next = it.next.nextn n

theorem String.eq_of_append_utf8Len {cs₁ cs₂ cs₃ cs₄ : List Char} (h₁ : cs₁ ++ cs₂ = cs₃ ++ cs₄) (h₂ : utf8Len cs₁ = utf8Len cs₃) : cs₁ = cs₃ ∧ cs₂ = cs₄

theorem String.eq_of_append_eq (l mr lm r : List Char) (le : utf8Len l ≤ utf8Len lm) (eq : l ++ mr = lm ++ r) : ∃ (m : List Char), mr = m ++ r ∧ lm = l ++ m

theorem String.Iterator.Valid.next' {it : Iterator} (v : it.Valid) (h : ¬it.atEnd = true) : it.next.Valid

theorem String.Iterator.Valid.of_isValid {it : Iterator} (v : Pos.isValid it.toString it.pos = true) : it.Valid

theorem String.Iterator.Valid.isValid {it : Iterator} (v : it.Valid) : Pos.isValid it.toString it.pos = true

theorem String.Iterator.Valid.validFor_of_valid_pos_le {it it' : Iterator} (v : it.Valid) (v' : it'.Valid) (eqs : it.toString = it'.toString) (le : it.pos ≤ it'.pos) : ∃ (l : List Char), ∃ (m : List Char), ∃ (r : List Char), ValidFor l.reverse (m ++ r) it ∧ ValidFor (m.reverse ++ l.reverse) r it'

theorem String.Iterator.Valid.pos_le_or_ge_next {it it' : Iterator} (v : it.Valid) (v' : it'.Valid) (eqs : it.toString = it'.toString) : it.pos ≤ it'.pos ∨ it'.next.pos ≤ it.pos

theorem String.Iterator.Valid.validFor_of_hasNext {it : Iterator} (h : it.hasNext = true) (v : it.Valid) : ∃ (l : List Char), ∃ (r : List Char), ValidFor l (it.curr :: r) it

theorem String.Iterator.ValidFor.eq {it : Iterator} {l₁ r₁ l₂ r₂ : List Char} (v₁ : ValidFor l₁ r₁ it) (v₂ : ValidFor l₂ r₂ it) : l₁ = l₂ ∧ r₁ = r₂

theorem String.Iterator.ValidFor.eq_it {it₁ it₂ : Iterator} {l r : List Char} (v₁ : ValidFor l r it₁) (v₂ : ValidFor l r it₂) : it₁ = it₂

theorem String.Iterator.ValidFor.exists_cons_of_not_atEnd {l r : List Char} {it : Iterator} (v : ValidFor l r it) (h : ¬it.atEnd = true) : ∃ (r' : List Char), r = it.curr :: r'

theorem String.Iterator.ValidFor.pos_atEnd {l : List Char} {it : Iterator} (v : ValidFor l [] it) : it.pos = it.toString.endPos

theorem String.Iterator.eq_of_valid_of_next_eq {it₁ it₂ : Iterator} (v₁ : it₁.Valid) (v₂ : it₂.Valid) (h : it₁.next = it₂.next) : it₁ = it₂

def String.Pos.ValidPlus (s : String) (p : Pos) : Prop

A variant of Valid that allows past-one position that represents the position after running a search at the end of the string.

Equations

• String.Pos.ValidPlus s p = (String.Pos.Valid s p ∨ p = s.endPos + { byteIdx := 1 })

theorem String.Pos.Valid.validPlus {s : String} {p : Pos} : Valid s p → ValidPlus s p

theorem String.Pos.next_endPos {s : String} : s.next s.endPos = s.endPos + { byteIdx := 1 }

theorem String.Pos.validPlus_of_next_valid {s : String} {p : Pos} (h : Valid s p) : ValidPlus s (s.next p)

theorem String.Pos.ValidPlus.valid_of_le {s : String} {p : Pos} (le : p ≤ s.endPos) (vp : ValidPlus s p) : Valid s p