Def String.repeat

Modification history

2022-03-01 10:48

Mathlib/Data/String/Defs.lean

chore: bump to nightly-2022-03-01 (#216)

Deleted String.repeat View on Github →

2021-10-11 17:57

Mathlib/Data/String/Defs.lean

feat(List/String leftpad) (#66)

Added String.repeat View on Github →