pad s : String
with repeated occurrences of c : Char
until it's of length n
.
If s
is initially larger than n
, just return s
.
Equations
- String.leftpad n c s = { data := List.leftpad n c s.data }
Equations
- String.replicate n c = { data := List.replicate n c }
Equations
- String.isPrefix x x = match x, x with | { data := d1 }, { data := d2 } => d1 <+: d2
Equations
- String.isSuffix x x = match x, x with | { data := d1 }, { data := d2 } => d1 <:+ d2
string.mapTokens c f s
tokenizes s : string
on c : char
, maps f
over each token, and
then reassembles the string by intercalating the separator token c
over the mapped tokens.
Equations
- String.mapTokens c f = String.intercalate (String.singleton c) ∘ List.map f ∘ fun x => String.split x fun x => decide (x = c)
isPrefixOf? pre s
returns some post
if s = pre ++ post
.
If pre
is not a prefix of s
, it returns none
.
Equations
- String.isPrefixOf? pre s = if String.startsWith s pre = true then some (String.drop s (String.length pre)) else none