Legacy implementations of String operations

This file includes old definitions of String functions that were downstreamed from core to prevent Batteries.Data.String.Lemmas from breaking.

@[irreducible, specialize #[]]

def String.Legacy.mapAux (f : Char → Char) (i : Pos.Raw) (s : String) : String

Implementation of String.Legacy.map.

Equations

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

@[inline]

def String.Legacy.map (f : Char → Char) (s : String) : String

Applies the function f to every character in a string, returning a string that contains the resulting characters.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.map.

Examples:

• "abc123".map Char.toUpper = "ABC123"
• "".map Char.toUpper = ""

Equations

• String.Legacy.map f s = String.Legacy.mapAux f 0 s