English
For every n and c, replicate(n,c) is the string consisting of n copies of c.
Русский
Для каждого n и символа c существует строка, состоящая из n копий символа c.
LaTeX
$$$ \forall n\in \mathbb{N},\forall c\in \text{Char},\text{replicate}(n,c) = \langle \text{List.replicate}(n,c) \rangle. $$$
Lean4
/-- Construct the string consisting of `n` copies of the character `c`. -/
def replicate (n : Nat) (c : Char) : String :=
⟨List.replicate n c⟩
-- TODO bring this definition in line with the above, either by:
-- adding `List.rightpad` to Batteries and changing the definition of `rightpad` here to match
-- or by changing the definition of `leftpad` above to match this
