instance instCoeStringSubstring_batteries : Coe String Substring

Equations

• instCoeStringSubstring_batteries = { coe := String.toSubstring }

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) (out : ByteArray) : ByteArray

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

Equations

• String.toAsciiByteArray.loop s p out = if h : s.atEnd p = true then out else let c := s.get p; let_fun this := ⋯; String.toAsciiByteArray.loop s (s.next p) (out.push c.toUInt8)