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.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy ↔ p₁ = p₂