theorem ByteArray.ext {a b : ByteArray} : a.data = b.data → a = b

theorem ByteArray.getElem_eq_data_getElem {i : Nat} (a : ByteArray) (h : i < a.size) : a[i] = a.data[i]

uget/uset

@[simp]

theorem ByteArray.uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) : a.uset i v h = a.set ⟨i.toNat, h⟩ v

empty

@[simp]

theorem ByteArray.data_mkEmpty (cap : Nat) : (ByteArray.mkEmpty cap).data = #[]

@[deprecated ByteArray.data_mkEmpty]

theorem ByteArray.mkEmpty_data (cap : Nat) : (ByteArray.mkEmpty cap).data = #[]

Alias of ByteArray.data_mkEmpty.

@[simp]

theorem ByteArray.data_empty : ByteArray.empty.data = #[]

@[deprecated ByteArray.data_empty]

theorem ByteArray.empty_data : ByteArray.empty.data = #[]

Alias of ByteArray.data_empty.

@[simp]

theorem ByteArray.size_empty : ByteArray.empty.size = 0

push

@[simp]

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

@[deprecated ByteArray.data_push]

theorem ByteArray.push_data (a : ByteArray) (b : UInt8) : (a.push b).data = a.data.push b

Alias of ByteArray.data_push.

@[simp]

theorem ByteArray.size_push (a : ByteArray) (b : UInt8) : (a.push b).size = a.size + 1

@[simp]

theorem ByteArray.get_push_eq (a : ByteArray) (x : UInt8) : (a.push x)[a.size] = x

theorem ByteArray.get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) : (a.push x)[i] = a[i]

set

@[simp]

theorem ByteArray.data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v).data = a.data.set i v

@[deprecated ByteArray.data_set]

theorem ByteArray.set_data (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v).data = a.data.set i v

Alias of ByteArray.data_set.

@[simp]

theorem ByteArray.size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v).size = a.size

@[simp]

theorem ByteArray.get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v)[↑i] = v

theorem ByteArray.get_set_ne {j : Nat} (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size) (h : ↑i ≠ j) : (a.set i v)[j] = a[j]

theorem ByteArray.set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) : (a.set i v).set ⟨↑i, ⋯⟩ v' = a.set i v'

copySlice

@[simp]

theorem ByteArray.data_copySlice (a : ByteArray) (i : Nat) (b : ByteArray) (j len : Nat) (exact : Bool) : (a.copySlice i b j len exact).data = b.data.extract 0 j ++ a.data.extract i (i + len) ++ b.data.extract (j + min len (a.data.size - i)) b.data.size

@[deprecated ByteArray.data_copySlice]

theorem ByteArray.copySlice_data (a : ByteArray) (i : Nat) (b : ByteArray) (j len : Nat) (exact : Bool) : (a.copySlice i b j len exact).data = b.data.extract 0 j ++ a.data.extract i (i + len) ++ b.data.extract (j + min len (a.data.size - i)) b.data.size

Alias of ByteArray.data_copySlice.

append

@[simp]

theorem ByteArray.append_eq (a b : ByteArray) : a.append b = a ++ b

@[simp]

theorem ByteArray.data_append (a b : ByteArray) : (a ++ b).data = a.data ++ b.data

@[deprecated ByteArray.data_append]

theorem ByteArray.append_data (a b : ByteArray) : (a ++ b).data = a.data ++ b.data

Alias of ByteArray.data_append.

theorem ByteArray.size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size

theorem ByteArray.get_append_left {i : Nat} {a b : ByteArray} (hlt : i < a.size) (h : i < (a ++ b).size := ⋯) : (a ++ b)[i] = a[i]

theorem ByteArray.get_append_right {i : Nat} {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size) (h' : i - a.size < b.size := ⋯) : (a ++ b)[i] = b[i - a.size]

extract

@[simp]

theorem ByteArray.data_extract (a : ByteArray) (start stop : Nat) : (a.extract start stop).data = a.data.extract start stop

@[deprecated ByteArray.data_extract]

theorem ByteArray.extract_data (a : ByteArray) (start stop : Nat) : (a.extract start stop).data = a.data.extract start stop

Alias of ByteArray.data_extract.

@[simp]

theorem ByteArray.size_extract (a : ByteArray) (start stop : Nat) : (a.extract start stop).size = min stop a.size - start

theorem ByteArray.get_extract_aux {i : Nat} {a : ByteArray} {start stop : Nat} (h : i < (a.extract start stop).size) : start + i < a.size

@[simp]

theorem ByteArray.get_extract {i : Nat} {a : ByteArray} {start stop : Nat} (h : i < (a.extract start stop).size) : (a.extract start stop)[i] = a[start + i]

ofFn

def ByteArray.ofFn {n : Nat} (f : Fin n → UInt8) : ByteArray

• ofFn f with f : Fin n → UInt8 returns the byte array whose ith element is f i. -

Equations

• ByteArray.ofFn f = { data := Array.ofFn f }

@[simp]

theorem ByteArray.data_ofFn {n : Nat} (f : Fin n → UInt8) : (ByteArray.ofFn f).data = Array.ofFn f

@[deprecated ByteArray.data_ofFn]

theorem ByteArray.ofFn_data {n : Nat} (f : Fin n → UInt8) : (ByteArray.ofFn f).data = Array.ofFn f

Alias of ByteArray.data_ofFn.

@[simp]

theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) : (ByteArray.ofFn f).size = n

@[simp]

theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ByteArray.ofFn f).size) : (ByteArray.ofFn f).get i = f (Fin.cast ⋯ i)

@[simp]

theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < (ByteArray.ofFn f).size) : (ByteArray.ofFn f)[i] = f ⟨i, ⋯⟩

map/mapM

@[inline]

unsafe def ByteArray.mapMUnsafe {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) : m ByteArray

Unsafe optimized implementation of mapM.

This function is unsafe because it relies on the implementation limit that the size of an array is always less than USize.size.

@[specialize #[]]

unsafe def ByteArray.mapMUnsafe.loop {m : Type → Type u_1} [Monad m] (f : UInt8 → m UInt8) (a : ByteArray) (k s : USize) : m ByteArray

Inner loop for mapMUnsafe.

@[implemented_by ByteArray.mapMUnsafe]

def ByteArray.mapM {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) : m ByteArray

mapM f a applies the monadic function f to each element of the array.

Equations

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

@[inline]

def ByteArray.map (a : ByteArray) (f : UInt8 → UInt8) : ByteArray

map f a applies the function f to each element of the array.

Equations

• a.map f = a.mapM f