mathlib documentation

s.split_on c tokenizes s : string on c : char.

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.

Tests whether the first string is a prefix of the second string.

Tests whether the first string is a suffix of the second string.

x.starts_with y is true if y is a prefix of x, and is false otherwise.

x.ends_with y is true if y is a suffix of x, and is false otherwise.

get_rest s t returns some r if s = t ++ r. If t is not a prefix of s, returns none

Removes the first n elements from the string s