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.

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

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

Equations

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
@[reducible]
def string.starts_with (x y : string) :

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

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

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 (s : string) (n : ) :

Removes the first n elements from the string s

Equations
def string.is_nat (s : string) :

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

Equations
def string.head (s : string) :

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

Equations