mathlib documentation

data.string.defs

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

Equations
def string.map_tokens  :
char(stringstring)stringstring

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

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

Equations

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

Equations

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

Equations
def string.popn  :
stringstring

Removes the first n elements from the string s

Equations
def string.is_nat  :

is_nat s is true iff s is a nonempty sequence of digits.

Equations