Documentation

Mathlib.Data.String.Lemmas

Miscellaneous lemmas about strings #

theorem String.congr_append (a : String) (b : String) :
a ++ b = { data := a.data ++ b.data }
@[simp]
theorem String.length_replicate (n : ) (c : Char) :
(String.replicate n c).length = n
theorem String.length_eq_list_length (l : List Char) :
{ data := l }.length = l.length
@[simp]
theorem String.leftpad_length (n : ) (c : Char) (s : String) :
(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

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