instance instCoeStringSubstring_batteries : Coe String Substring

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

Count the occurrences of a character in a string.

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.

@[irreducible]

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

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