@[instance_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