Documentation

Batteries.Data.ByteArray

source
🔸 coverage
@[implicit_reducible]
instance ByteArray.instDecidableEq_batteries :
DecidableEq ByteArray
Equations
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) :
(emptyWithCapacity cap).data = #[]

push #

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.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
📐 coverage
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))

append #

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
theorem ByteArray.get_extract_aux {i : Nat} {a : ByteArray} {start stop : Nat} (h : i < (a.extract start stop).size) :
start + i < a.size
source
📐 coverage
@[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
🔸 coverage
@[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.emptyWithCapacity n)
Instances For
    source
    📐 coverage
    @[simp]
    theorem ByteArray.ofFn_zero (f : Fin 0 → UInt8) :
    ofFn f = empty
    source
    📐 coverage
    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))
    source
    📐 coverage
    @[simp]
    theorem ByteArray.data_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).data = Array.ofFn f
    source
    📐 coverage
    @[simp]
    theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).size = n
    source
    📐 coverage
    @[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
    📐 coverage
    @[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
    🔸 coverage
    @[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
      🔸 coverage
      @[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
        🔸 coverage
        @[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
          🔸 coverage
          @[inline]
          def ByteArray.map (a : ByteArray) (f : UInt8 → UInt8) :
          ByteArray

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

          Equations
          Instances For