Documentation

Mathlib.Data.String.Defs

def String.leftpad (n : Nat) (c : Char) (s : String) :

pad s : String with repeated occurrences of c : Char until it's of length n. If s is initially larger than n, just return s.

Equations
def String.replicate (n : Nat) (c : Char) :
Equations
Equations
Equations
def String.mapTokens (c : Char) (f : StringString) :

string.mapTokens 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

isPrefixOf? pre s returns some post if s = pre ++ post. If pre is not a prefix of s, it returns none.

Equations