Documentation

Init.Data.ByteArray.Basic

source
structure ByteArray:
Type
source
@[extern lean_mk_empty_byte_array]
def ByteArray.mkEmpty (c : Nat) :
ByteArray
Equations
source
def ByteArray.empty:
ByteArray
Equations
source
instance ByteArray.instInhabitedByteArray:
Inhabited ByteArray
Equations
source
instance ByteArray.instEmptyCollectionByteArray:
EmptyCollection ByteArray
Equations
source
@[extern lean_byte_array_push]
def ByteArray.push:
ByteArray → UInt8 → ByteArray
Equations
source
@[extern lean_byte_array_size]
def ByteArray.size:
ByteArray → Nat
Equations
source
@[extern lean_byte_array_uget]
def ByteArray.uget (a : ByteArray) (i : USize) :
USize.toNat i < ByteArray.size a → UInt8
Equations
  • ByteArray.uget _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, h => Array.uget bs i h
source
@[extern lean_byte_array_get]
def ByteArray.get!:
ByteArray → Nat → UInt8
Equations
source
@[extern lean_byte_array_fget]
def ByteArray.get (a : ByteArray) :
Fin (ByteArray.size a) → UInt8
Equations
source
@[inline]
def ByteArray.getOp (self : ByteArray) (idx : Nat) :
UInt8
Equations
source
@[extern lean_byte_array_set]
def ByteArray.set!:
ByteArray → Nat → UInt8 → ByteArray
Equations
  • ByteArray.set! _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, b => { data := Array.set! bs i b }
source
@[extern lean_byte_array_fset]
def ByteArray.set (a : ByteArray) :
Fin (ByteArray.size a) → UInt8 → ByteArray
Equations
  • ByteArray.set _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, b => { data := Array.set bs i b }
source
@[extern lean_byte_array_uset]
def ByteArray.uset (a : ByteArray) (i : USize) :
(a : UInt8) → USize.toNat i < ByteArray.size a → ByteArray
Equations
  • ByteArray.uset _fun_discr _fun_discr _fun_discr _fun_discr = match _fun_discr, _fun_discr, _fun_discr, _fun_discr with | { data := bs }, i, v, h => { data := Array.uset bs i v h }
source
def ByteArray.isEmpty (s : ByteArray) :
Bool
Equations
source
@[extern lean_byte_array_copy_slice]
def ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff : Nat) (len : Nat) (exact : optParam Bool true) :
ByteArray

Copy the slice at [srcOff, srcOff + len) in src to [destOff, destOff + len) in dest, growing dest if necessary. If exact is false, the capacity will be doubled when grown.

Equations
  • One or more equations did not get rendered due to their size.
source
def ByteArray.extract (a : ByteArray) (b : Nat) (e : Nat) :
ByteArray
Equations
source
def ByteArray.append (a : ByteArray) (b : ByteArray) :
ByteArray
Equations
source
instance ByteArray.instAppendByteArray:
Append ByteArray
Equations
source
def ByteArray.toList (bs : ByteArray) :
List UInt8
Equations
source
partial def ByteArray.toList.loop (bs : ByteArray) (i : Nat) (r : List UInt8) :
List UInt8
source
@[inline]
def ByteArray.findIdx? (a : ByteArray) (p : UInt8 → Bool) (start : optParam Nat 0) :
Option Nat
Equations
source
@[specialize]
partial def ByteArray.findIdx?.loop (a : ByteArray) (p : UInt8 → Bool) (i : Nat) :
Option Nat
source
@[inline]
unsafe def ByteArray.forInUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) :
m β
Equations
source
@[specialize]
unsafe def ByteArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (sz : USize) (i : USize) (b : β) :
m β
Equations
  • One or more equations did not get rendered due to their size.
source
@[implementedBy ByteArray.forInUnsafe]
def ByteArray.forIn {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) :
m β
Equations
source
def ByteArray.forIn.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (i : Nat) (h : i ≤ ByteArray.size as) (b : β) :
m β
Equations
source
instance ByteArray.instForInByteArrayUInt8 {m : Type u_1 → Type u_2} :
ForIn m ByteArray UInt8
Equations
  • ByteArray.instForInByteArrayUInt8 = { forIn := fun {β} [Monad m] => ByteArray.forIn }
source
@[inline]
unsafe def ByteArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) :
m β
Equations
  • One or more equations did not get rendered due to their size.
source
@[specialize]
unsafe def ByteArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (as : ByteArray) (i : USize) (stop : USize) (b : β) :
m β
Equations
  • One or more equations did not get rendered due to their size.
source
@[implementedBy ByteArray.foldlMUnsafe]
def ByteArray.foldlM {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) :
m β
Equations
  • One or more equations did not get rendered due to their size.
source
def ByteArray.foldlM.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (as : ByteArray) (stop : Nat) (h : stop ≤ ByteArray.size as) (i : Nat) (j : Nat) (b : β) :
m β
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def ByteArray.foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) :
β
Equations
source
def List.toByteArray (bs : List UInt8) :
ByteArray
Equations
source
def List.toByteArray.loop:
List UInt8 → ByteArray → ByteArray
Equations
source
instance instToStringByteArray:
ToString ByteArray
Equations
source
def ByteArray.toUInt64LE! (bs : ByteArray) :
UInt64

Interpret a ByteArray of size 8 as a little-endian UInt64.

Equations
  • One or more equations did not get rendered due to their size.
source
def ByteArray.toUInt64BE! (bs : ByteArray) :
UInt64

Interpret a ByteArray of size 8 as a big-endian UInt64.

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