ink

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 = { data := List.leftpad n c s.data }

ink

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

Equations

• String.replicate n c = { data := List.replicate n c }

ink

def String.isPrefix : String → String → Prop

Equations

• String.isPrefix x x = match x, x with | { data := d1 }, { data := d2 } => d1 <+: d2

ink

def String.isSuffix : String → String → Prop

Equations

• String.isSuffix x x = match x, x with | { data := d1 }, { data := d2 } => d1 <:+ d2

ink

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.intercalate (String.singleton c) ∘ List.map f ∘ fun x => String.split x fun x => decide (x = c)

ink

def String.isPrefixOf? (pre : String) (s : String) : Option String

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

Equations

• String.isPrefixOf? pre s = if String.startsWith s pre = true then some (String.drop s (String.length pre)) else none