Documentation

Batteries.Data.ByteArray

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

uget/uset #

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

source
@[simp]
theorem ByteArray.data_mkEmpty (cap : Nat) :
(mkEmpty cap).data = #[]
source
@[deprecated ByteArray.data_mkEmpty (since := "2024-08-13")]
theorem ByteArray.mkEmpty_data (cap : Nat) :
(mkEmpty cap).data = #[]

Alias of ByteArray.data_mkEmpty.

source
@[simp]
theorem ByteArray.data_empty :
empty.data = #[]
source
@[deprecated ByteArray.data_empty (since := "2024-08-13")]
theorem ByteArray.empty_data :
empty.data = #[]

Alias of ByteArray.data_empty.

source
@[simp]
theorem ByteArray.size_empty :
empty.size = 0

push #

source
@[simp]
theorem ByteArray.data_push (a : ByteArray) (b : UInt8) :
(a.push b).data = a.data.push b
source
@[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.

source
@[simp]
theorem ByteArray.size_push (a : ByteArray) (b : UInt8) :
(a.push b).size = a.size + 1
source
@[simp]
theorem ByteArray.get_push_eq (a : ByteArray) (x : UInt8) :
(a.push x)[a.size] = x
source
theorem ByteArray.get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
(a.push x)[i] = a[i]

set #

source
@[simp]
theorem ByteArray.data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
(a.set (↑i) v ⋯).data = a.data.set (↑i) v ⋯
source
@[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.

source
@[simp]
theorem ByteArray.size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
(a.set (↑i) v ⋯).size = a.size
source
@[simp]
theorem ByteArray.get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) :
(a.set (↑i) v ⋯)[↑i] = v
source
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]
source
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 #

source
@[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
source
@[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)) b.data.size

Alias of ByteArray.data_copySlice.

append #

source
@[simp]
theorem ByteArray.append_eq (a b : ByteArray) :
a.append b = a ++ b
source
@[simp]
theorem ByteArray.data_append (a b : ByteArray) :
(a ++ b).data = a.data ++ b.data
source
@[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.

source
theorem ByteArray.size_append (a b : ByteArray) :
(a ++ b).size = a.size + b.size
source
theorem ByteArray.get_append_left {i : Nat} {a b : ByteArray} (hlt : i < a.size) (h : i < (a ++ b).size := ⋯) :
(a ++ b)[i] = a[i]
source
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 #

source
@[simp]
theorem ByteArray.data_extract (a : ByteArray) (start stop : Nat) :
(a.extract start stop).data = a.data.extract start stop
source
@[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.

source
@[simp]
theorem ByteArray.size_extract (a : ByteArray) (start stop : Nat) :
(a.extract start stop).size = min stop a.size - start
source
theorem ByteArray.get_extract_aux {i : Nat} {a : ByteArray} {start stop : Nat} (h : i < (a.extract start stop).size) :
start + i < a.size
source
@[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 #

source
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
Instances For
    source
    @[simp]
    theorem ByteArray.data_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).data = Array.ofFn f
    source
    @[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.

    source
    @[simp]
    theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).size = n
    source
    @[simp]
    theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ofFn f).size) :
    (ofFn f).get ↑i ⋯ = f (Fin.cast ⋯ i)
    source
    @[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 #

    source
    @[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
    Instances For
      source
      @[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.
      Instances For
        source
        @[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.
        Instances For
          source
          @[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
          Instances For