Miscellaneous lemmas about strings

theorem String.congr_append (a b : String) : a ++ b = { data := a.data ++ b.data }

@[simp]

theorem String.length_replicate (n : ℕ) (c : Char) : (replicate n c).length = n

theorem String.length_eq_list_length (l : List Char) : { data := l }.length = l.length

@[simp]

theorem String.length_leftpad (n : ℕ) (c : Char) (s : String) : (leftpad n c s).length = max n s.length

The length of the String returned by String.leftpad n a c is equal to the larger of n and s.length

@[deprecated String.length_leftpad (since := "2025-02-24")]

theorem String.leftpad_length (n : ℕ) (c : Char) (s : String) : (leftpad n c s).length = max n s.length

Alias of String.length_leftpad.

---

The length of the String returned by String.leftpad n a c is equal to the larger of n and s.length

theorem String.leftpad_prefix (n : ℕ) (c : Char) (s : String) : (replicate (n - s.length) c).IsPrefix (leftpad n c s)

theorem String.leftpad_suffix (n : ℕ) (c : Char) (s : String) : s.IsSuffix (leftpad n c s)