Definitions for String

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

def Char.isAscii (c : Char) : Bool

Determine if a unicode character is part of the ASCII subset.

ASCII characters have code points in the range U+0000-U+007F. (Note: the Unicode standard) does not mention ASCII and instead calls this subset "C0 Controls and Basic Latin".)

def String.leftpad (n : Nat) (c : Char := ' ') (s : String) : 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.

def String.replicate (n : Nat) (c : Char) : String

Construct the string consisting of n copies of the character c.

def String.rightpad (n : Nat) (c : Char := ' ') (s : String) : String

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

def String.IsPrefix : String → String → Prop

s.IsPrefix t checks if the string s is a prefix of the string t.

def String.IsSuffix : String → String → Prop

s.IsSuffix t checks if the string s is a suffix of the string t.

def String.mapTokens (c : Char) (f : String → String) : String → String

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.

def String.head (s : String) : Char

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