Basic lemmas about strings

This file contains lemmas that could be in Init.Data.String.Basic but are not because they are not needed to define basic string operations.

@[simp]

theorem String.singleton_append_inj {c : Char} {s : String} {d : Char} {t : String} : singleton c ++ s = singleton d ++ t ↔ c = d ∧ s = t

@[simp]

theorem String.push_inj {s : String} {c : Char} {t : String} {d : Char} : s.push c = t.push d ↔ s = t ∧ c = d

@[simp]

theorem String.append_eq_empty_iff {s t : String} : s ++ t = "" ↔ s = "" ∧ t = ""

@[simp]

theorem String.push_ne_empty {s : String} {c : Char} : s.push c ≠ ""

@[simp]

theorem String.singleton_ne_empty {c : Char} : singleton c ≠ ""

@[simp]

theorem String.Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂

@[simp]

theorem String.Pos.startPos_le {s : String} (p : s.Pos) : s.startPos ≤ p

@[simp]

theorem String.Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p

@[simp]

theorem String.Slice.Pos.le_endPos {s : Slice} (p : s.Pos) : p ≤ s.endPos