@[simp]

theorem ByteArray.data_push {a : ByteArray} {b : UInt8} : (a.push b).data = a.data.push b

def ByteArray.append (a b : ByteArray) : ByteArray

Appends two byte arrays.

In compiled code, calls to ByteArray.append are replaced with the much more efficient ByteArray.fastAppend.

Equations

• a.append b = { data := { toList := a.data.toList ++ b.data.toList } }

@[simp]

theorem ByteArray.toList_data_append' {a b : ByteArray} : (a.append b).data.toList = a.data.toList ++ b.data.toList

theorem ByteArray.ext {x y : ByteArray} : x.data = y.data → x = y

@[simp]

theorem List.toList_data_toByteArray {l : List UInt8} : l.toByteArray.data.toList = l

theorem List.toByteArray_append' {l l' : List UInt8} : (l ++ l').toByteArray = l.toByteArray.append l'.toByteArray