@[implicit_reducible]

instance instCoeStringRaw_batteries : Coe String Substring.Raw

Equations

• instCoeStringRaw_batteries = { coe := String.toRawSubstring }

def String.count (s : String) (c : Char) : Nat

Count the occurrences of a character in a string.

Equations

• s.count c = String.foldl (fun (n : Nat) (d : Char) => if d = c then n + 1 else n) 0 s

def String.toAsciiByteArray (s : String) : ByteArray

Convert a string of assumed-ASCII characters into a byte array. (If any characters are non-ASCII they will be reduced modulo 256.)

Note: if you just need the underlying ByteArray of a non-ASCII string, use String.toUTF8.

Equations

• s.toAsciiByteArray = String.toAsciiByteArray.loop s 0 ByteArray.empty

@[irreducible]

def String.toAsciiByteArray.loop (s : String) (p : Pos.Raw) (out : ByteArray) : ByteArray

Internal implementation of toAsciiByteArray. loop p out = out ++ toAsciiByteArray ({ s with startPos := p } : Substring)

Equations

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