mathlib3 documentation

data.string.defs

Definitions for string #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a bunch of functions for the string datatype.

source
def string.split_on (s : string) (c : char) :
list string

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

Equations
source
def string.map_tokens (c : char) (f : string → string) :
string → string

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
source
def string.is_prefix_of (x y : string) :
bool

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

Equations
source
def string.is_suffix_of (x y : string) :
bool

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

Equations
source
@[reducible]
def string.starts_with (x y : string) :
bool

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

source
@[reducible]
def string.ends_with (x y : string) :
bool

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

source
def string.get_rest (s t : string) :
option string

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

Equations
source
def string.popn (s : string) (n : ℕ) :
string

Removes the first n elements from the string s

Equations
source
def string.is_nat (s : string) :
bool

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

Equations
source
def string.head (s : string) :
char

Produce the head character from the string s, if s is not empty, otherwise 'A'.

Equations