String helpers

Small string operations used across the library, written over List Char so they do not depend on the String/String.Slice API, which changes between Lean releases.

def TypeDB.Str.dropRight (s : String) (n : Nat) : String

Equations

• TypeDB.Str.dropRight s n = String.ofList (List.take (s.length - n) s.toList)

def TypeDB.Str.takeRight (s : String) (n : Nat) : String

Equations

• TypeDB.Str.takeRight s n = String.ofList (List.drop (s.length - n) s.toList)

def TypeDB.Str.dropLeft (s : String) (n : Nat) : String

Equations

• TypeDB.Str.dropLeft s n = String.ofList (List.drop n s.toList)

def TypeDB.Str.dropRightWhile (s : String) (p : Char → Bool) : String

Equations

• TypeDB.Str.dropRightWhile s p = String.ofList (List.dropWhile p s.toList.reverse).reverse

def TypeDB.Str.dropLeftWhile (s : String) (p : Char → Bool) : String

Equations

• TypeDB.Str.dropLeftWhile s p = String.ofList (List.dropWhile p s.toList)

def TypeDB.Str.trim (s : String) : String

Equations

• TypeDB.Str.trim s = TypeDB.Str.dropRightWhile (TypeDB.Str.dropLeftWhile s Char.isWhitespace) Char.isWhitespace

def TypeDB.Str.padLeft (s : String) (width : Nat) (c : Char) : String

Equations

• TypeDB.Str.padLeft s width c = "".pushn c (width - s.length) ++ s

def TypeDB.Str.contains (s sub : String) : Bool

Whether sub occurs in s.

Equations

• TypeDB.Str.contains s sub = decide ((s.splitOn sub).length > 1)

def TypeDB.Str.kebab (s : String) : String

kebab-case of a CamelCase identifier: FriendRequest ↦ friend-request.

Equations

• One or more equations did not get rendered due to their size.