# Documentation

Mathlib.Data.String.Lemmas

theorem String.congr_append (a : String) (b : String) :
a ++ b = { data := a.data ++ b.data }
@[simp]
theorem String.length_append (as : String) (bs : String) :
String.length (as ++ bs) =
@[simp]
theorem String.length_replicate (n : ) (c : Char) :
= n
@[simp]
theorem String.leftpad_length (n : ) (c : Char) (s : String) :

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