Zulip Chat Archive
Stream: lean4
Topic: String repeating a character
Patrick Massot (Sep 19 2023 at 14:41):
What is the official way of doing
def String.mkSpace : Nat → String
| 0 => ""
| n + 1 => " " ++ mkSpace n
possibly with another character instead of space?
Alex J. Best (Sep 19 2023 at 14:48):
Patrick Massot (Sep 19 2023 at 14:51):
Thanks! I guess this whole file should migrate to Std...
Last updated: Dec 20 2023 at 11:08 UTC