@[extern lean_byte_array_uget]
Instances For
@[extern lean_byte_array_fget]
Instances For
@[extern lean_byte_array_fset]
Instances For
@[extern lean_byte_array_uset]
def
ByteArray.uset
(a : ByteArray)
(i : USize)
:
UInt8 → USize.toNat i < ByteArray.size a → ByteArray
Instances For
@[extern lean_byte_array_copy_slice]
def
ByteArray.copySlice
(src : ByteArray)
(srcOff : Nat)
(dest : ByteArray)
(destOff : Nat)
(len : Nat)
(exact : optParam Bool true)
:
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.
Instances For
@[inline]
unsafe def
ByteArray.forInUnsafe
{β : Type v}
{m : Type v → Type w}
[Monad m]
(as : ByteArray)
(b : β)
(f : UInt8 → β → m (ForInStep β))
:
m β
We claim this unsafe implementation is correct because an array cannot have more than usizeSz
elements in our runtime.
This is similar to the Array
version.
TODO: avoid code duplication in the future after we improve the compiler.
Instances For
def
ByteArray.forIn.loop
{β : Type v}
{m : Type v → Type w}
[Monad m]
(as : ByteArray)
(f : UInt8 → β → m (ForInStep β))
(i : Nat)
(h : i ≤ ByteArray.size as)
(b : β)
:
m β
Equations
- One or more equations did not get rendered due to their size.
- ByteArray.forIn.loop as f 0 x b = pure b
Instances For
@[inline]
unsafe def
ByteArray.foldlMUnsafe
{β : Type v}
{m : Type v → Type w}
[Monad m]
(f : β → UInt8 → m β)
(init : β)
(as : ByteArray)
(start : optParam Nat 0)
(stop : optParam Nat (ByteArray.size as))
:
m β
See comment at forInUnsafe
Instances For
@[inline]
def
ByteArray.foldl
{β : Type v}
(f : β → UInt8 → β)
(init : β)
(as : ByteArray)
(start : optParam Nat 0)
(stop : optParam Nat (ByteArray.size as))
:
β
Instances For
Equations
- List.toByteArray.loop [] x = x
- List.toByteArray.loop (b :: bs) x = List.toByteArray.loop bs (ByteArray.push x b)