theorem ByteArray.ext {x y : ByteArray} (data : x.data = y.data) : x = y

instance ByteArray.instDecidableEq_batteries : DecidableEq ByteArray

Equations

• x✝¹.instDecidableEq_batteries x✝ = decidable_of_decidable_of_iff ⋯

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 v h

empty

@[simp]

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

@[deprecated ByteArray.data_mkEmpty (since := "2024-08-13")]

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

Alias of ByteArray.data_mkEmpty.

@[simp]

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

@[deprecated ByteArray.data_empty (since := "2024-08-13")]

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

Alias of ByteArray.data_empty.

@[simp]

theorem ByteArray.size_empty : 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 (since := "2024-08-13")]

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 (since := "2024-08-13")]

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))

@[deprecated ByteArray.data_copySlice (since := "2024-08-13")]

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))

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 (since := "2024-08-13")]

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 (since := "2024-08-13")]

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

@[inline]

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 = Fin.foldl n (fun (acc : ByteArray) (i : Fin n) => acc.push (f i)) (ByteArray.mkEmpty n)

@[simp]

theorem ByteArray.ofFn_zero (f : Fin 0 → UInt8) : ofFn f = empty

theorem ByteArray.ofFn_succ {n : Nat} (f : Fin (n + 1) → UInt8) : ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f (Fin.last n))

@[simp]

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

@[deprecated ByteArray.data_ofFn (since := "2024-08-13")]

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

Alias of ByteArray.data_ofFn.

@[simp]

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

@[simp]

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

@[simp]

theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < (ofFn f).size) : (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.

Equations

• a.mapMUnsafe f = ByteArray.mapMUnsafe.loop f a 0 a.usize

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

Equations

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

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