# Definitions for `String` #

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

source
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`.

Equations

- String.leftpad n c s = (List.leftpad n c s.data).asString

Instances For

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

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

Equations

- String.replicate n c = (List.replicate n c).asString

Instances For

source
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`.

Equations

- String.rightpad n c s = s ++ String.replicate (n - s.length) c

Instances For

source
def String.IsPrefix :
String → String → Prop

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

Equations

- x✝¹.IsPrefix x✝ = (x✝¹.data <+: x✝.data)

Instances For

source
def String.IsSuffix :
String → String → Prop

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

Equations

- x✝¹.IsSuffix x✝ = (x✝¹.data <:+ x✝.data)

Instances For

source
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.

Equations

- String.mapTokens c f = (String.singleton c).intercalate ∘ List.map f ∘ fun (x : String) => x.splitToList fun (x : Char) => decide (x = c)

Instances For

source
def String.head (s : String) :
Char

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

Equations

- s.head = s.iter.curr

Instances For