s.split_on c
tokenizes s : string
on c : char
.
Equations
- s.split_on c = string.split (λ (_x : char), decidable.to_bool (_x = c)) s
string.map_tokens 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.map_tokens c f = (string.singleton c).intercalate ∘ list.map f ∘ string.split (λ (_x : char), decidable.to_bool (_x = c))
Tests whether the first string is a prefix of the second string.
Equations
- x.is_prefix_of y = x.to_list.is_prefix_of y.to_list
Tests whether the first string is a suffix of the second string.
Equations
- x.is_suffix_of y = x.to_list.is_suffix_of y.to_list
@[reducible]
x.starts_with y
is true if y
is a prefix of x
, and is false otherwise.
@[reducible]
x.ends_with y
is true if y
is a suffix of x
, and is false otherwise.
Removes the first n
elements from the string s
Equations
- s.popn n = (s.mk_iterator.nextn n).next_to_string
Produce the head character from the string s
, if s
is not empty, otherwise 'A'.
Equations
- s.head = s.mk_iterator.curr