Byte order

Conversions between the arrays with elements wider than a byte and ByteArray, in little-endian (LE, least significant byte first) or big-endian (BE, most significant byte first) order, and in-place byte swaps of the integer arrays. Floats are converted through their IEEE 754 bits. Slice.ofBytes… reads the bytes of a UInt8Array.Slice instead, such as the part of a ByteArray after a header, without copying the rest.

The results do not depend on the byte order of the machine. That byte order is computed once, when the module is initialized: when a conversion asks for the machine's own order, it copies the whole array at once. Otherwise ofBytes… copies and then swaps the bytes of each element in place, and toBytes… is a loop of shifts and byte accesses, which the C compiler turns into whole-word loads, stores and byte swap instructions.

Experimental. The names and types here may still change. import ScalarArray does not import this module; use import ScalarArray.Bytes.

This module is generated by scripts/generate.py; edit scripts/bytes_template.py instead.

@[inline]

def UInt16.byteSwap (x : UInt16) : UInt16

Reverses the order of the bytes of x.

Equations

• x.byteSwap = x >>> 8 ||| x <<< 8

@[inline]

def UInt32.byteSwap (x : UInt32) : UInt32

Reverses the order of the bytes of x.

Equations

• x.byteSwap = ((x &&& 16711935) <<< 8 ||| x >>> 8 &&& 16711935) >>> 16 ||| ((x &&& 16711935) <<< 8 ||| x >>> 8 &&& 16711935) <<< 16

@[inline]

def UInt64.byteSwap (x : UInt64) : UInt64

Reverses the order of the bytes of x.

Equations

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

@[inline]

def Int16.byteSwap (x : Int16) : Int16

Reverses the order of the bytes of x.

Equations

• x.byteSwap = x.toUInt16.byteSwap.toInt16

@[inline]

def Int32.byteSwap (x : Int32) : Int32

Reverses the order of the bytes of x.

Equations

• x.byteSwap = x.toUInt32.byteSwap.toInt32

@[inline]

def Int64.byteSwap (x : Int64) : Int64

Reverses the order of the bytes of x.

Equations

• x.byteSwap = x.toUInt64.byteSwap.toInt64

@[simp]

theorem UInt16.byteSwap_byteSwap (x : UInt16) : x.byteSwap.byteSwap = x

@[simp]

theorem UInt32.byteSwap_byteSwap (x : UInt32) : x.byteSwap.byteSwap = x

@[simp]

theorem UInt64.byteSwap_byteSwap (x : UInt64) : x.byteSwap.byteSwap = x

@[simp]

theorem Int16.byteSwap_byteSwap (x : Int16) : x.byteSwap.byteSwap = x

@[simp]

theorem Int32.byteSwap_byteSwap (x : Int32) : x.byteSwap.byteSwap = x

@[simp]

theorem Int64.byteSwap_byteSwap (x : Int64) : x.byteSwap.byteSwap = x

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.byteSwapImpl]

def ScalarArray.UInt16Array.byteSwap (a : UInt16Array) : UInt16Array

Reverses the order of the bytes of each element, in place when a is not shared.

Equations

• a.byteSwap = ScalarArray.UInt16Array.mk (Array.map UInt16.byteSwap a.toArray)

@[simp]

theorem ScalarArray.UInt16Array.toArray_byteSwap (a : UInt16Array) : a.byteSwap.toArray = Array.map UInt16.byteSwap a.toArray

@[simp]

theorem ScalarArray.UInt16Array.size_byteSwap (a : UInt16Array) : a.byteSwap.size = a.size

@[simp]

theorem ScalarArray.UInt16Array.getElem_byteSwap (a : UInt16Array) (i : Nat) (h : i < a.byteSwap.size) : a.byteSwap[i] = a[i].byteSwap

@[simp]

theorem ScalarArray.UInt16Array.byteSwap_byteSwap (a : UInt16Array) : a.byteSwap.byteSwap = a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.Slice.toBytesLEImpl]

def ScalarArray.UInt16Array.Slice.toBytesLE (s : UInt16Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (2 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 2] >>> (8 * (j % 2)).toUInt16).toUInt8 }

@[inline]

def ScalarArray.UInt16Array.toBytesLE (a : UInt16Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.ofBytesLE?Impl]

def ScalarArray.UInt16Array.ofBytesLE? (b : ByteArray) : Option UInt16Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 2.

Equations

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

def ScalarArray.UInt16Array.ofBytesLE! (b : ByteArray) : UInt16Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 2.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.Slice.ofBytesLE?Impl]

def ScalarArray.UInt16Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option UInt16Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 2.

Equations

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

def ScalarArray.UInt16Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : UInt16Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 2.

Equations

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

@[simp]

theorem ScalarArray.UInt16Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = UInt16Array.ofBytesLE? b

@[simp]

theorem ScalarArray.UInt16Array.Slice.size_toBytesLE (s : UInt16Array.Slice) : s.toBytesLE.size = 2 * Std.Slice.size s

@[simp]

theorem ScalarArray.UInt16Array.size_toBytesLE (a : UInt16Array) : a.toBytesLE.size = 2 * a.size

@[simp]

theorem ScalarArray.UInt16Array.Slice.getElem_toBytesLE (s : UInt16Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 2] >>> (8 * (j % 2)).toUInt16).toUInt8

@[simp]

theorem ScalarArray.UInt16Array.ofBytesLE?_toBytesLE_slice (s : UInt16Array.Slice) : ofBytesLE? s.toBytesLE = some s.copy

@[simp]

theorem ScalarArray.UInt16Array.ofBytesLE?_toBytesLE (a : UInt16Array) : ofBytesLE? a.toBytesLE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.Slice.toBytesBEImpl]

def ScalarArray.UInt16Array.Slice.toBytesBE (s : UInt16Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (2 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 2] >>> (8 * (1 - j % 2)).toUInt16).toUInt8 }

@[inline]

def ScalarArray.UInt16Array.toBytesBE (a : UInt16Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.ofBytesBE?Impl]

def ScalarArray.UInt16Array.ofBytesBE? (b : ByteArray) : Option UInt16Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 2.

Equations

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

def ScalarArray.UInt16Array.ofBytesBE! (b : ByteArray) : UInt16Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 2.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt16Array.Slice.ofBytesBE?Impl]

def ScalarArray.UInt16Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option UInt16Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 2.

Equations

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

def ScalarArray.UInt16Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : UInt16Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 2.

Equations

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

@[simp]

theorem ScalarArray.UInt16Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = UInt16Array.ofBytesBE? b

@[simp]

theorem ScalarArray.UInt16Array.Slice.size_toBytesBE (s : UInt16Array.Slice) : s.toBytesBE.size = 2 * Std.Slice.size s

@[simp]

theorem ScalarArray.UInt16Array.size_toBytesBE (a : UInt16Array) : a.toBytesBE.size = 2 * a.size

@[simp]

theorem ScalarArray.UInt16Array.Slice.getElem_toBytesBE (s : UInt16Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 2] >>> (8 * (1 - j % 2)).toUInt16).toUInt8

@[simp]

theorem ScalarArray.UInt16Array.ofBytesBE?_toBytesBE_slice (s : UInt16Array.Slice) : ofBytesBE? s.toBytesBE = some s.copy

@[simp]

theorem ScalarArray.UInt16Array.ofBytesBE?_toBytesBE (a : UInt16Array) : ofBytesBE? a.toBytesBE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.byteSwapImpl]

def ScalarArray.UInt32Array.byteSwap (a : UInt32Array) : UInt32Array

Reverses the order of the bytes of each element, in place when a is not shared.

Equations

• a.byteSwap = ScalarArray.UInt32Array.mk (Array.map UInt32.byteSwap a.toArray)

@[simp]

theorem ScalarArray.UInt32Array.toArray_byteSwap (a : UInt32Array) : a.byteSwap.toArray = Array.map UInt32.byteSwap a.toArray

@[simp]

theorem ScalarArray.UInt32Array.size_byteSwap (a : UInt32Array) : a.byteSwap.size = a.size

@[simp]

theorem ScalarArray.UInt32Array.getElem_byteSwap (a : UInt32Array) (i : Nat) (h : i < a.byteSwap.size) : a.byteSwap[i] = a[i].byteSwap

@[simp]

theorem ScalarArray.UInt32Array.byteSwap_byteSwap (a : UInt32Array) : a.byteSwap.byteSwap = a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.Slice.toBytesLEImpl]

def ScalarArray.UInt32Array.Slice.toBytesLE (s : UInt32Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (4 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 4] >>> (8 * (j % 4)).toUInt32).toUInt8 }

@[inline]

def ScalarArray.UInt32Array.toBytesLE (a : UInt32Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.ofBytesLE?Impl]

def ScalarArray.UInt32Array.ofBytesLE? (b : ByteArray) : Option UInt32Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 4.

Equations

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

def ScalarArray.UInt32Array.ofBytesLE! (b : ByteArray) : UInt32Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 4.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.Slice.ofBytesLE?Impl]

def ScalarArray.UInt32Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option UInt32Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 4.

Equations

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

def ScalarArray.UInt32Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : UInt32Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 4.

Equations

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

@[simp]

theorem ScalarArray.UInt32Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = UInt32Array.ofBytesLE? b

@[simp]

theorem ScalarArray.UInt32Array.Slice.size_toBytesLE (s : UInt32Array.Slice) : s.toBytesLE.size = 4 * Std.Slice.size s

@[simp]

theorem ScalarArray.UInt32Array.size_toBytesLE (a : UInt32Array) : a.toBytesLE.size = 4 * a.size

@[simp]

theorem ScalarArray.UInt32Array.Slice.getElem_toBytesLE (s : UInt32Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 4] >>> (8 * (j % 4)).toUInt32).toUInt8

@[simp]

theorem ScalarArray.UInt32Array.ofBytesLE?_toBytesLE_slice (s : UInt32Array.Slice) : ofBytesLE? s.toBytesLE = some s.copy

@[simp]

theorem ScalarArray.UInt32Array.ofBytesLE?_toBytesLE (a : UInt32Array) : ofBytesLE? a.toBytesLE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.Slice.toBytesBEImpl]

def ScalarArray.UInt32Array.Slice.toBytesBE (s : UInt32Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (4 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 4] >>> (8 * (3 - j % 4)).toUInt32).toUInt8 }

@[inline]

def ScalarArray.UInt32Array.toBytesBE (a : UInt32Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.ofBytesBE?Impl]

def ScalarArray.UInt32Array.ofBytesBE? (b : ByteArray) : Option UInt32Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 4.

Equations

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

def ScalarArray.UInt32Array.ofBytesBE! (b : ByteArray) : UInt32Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 4.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt32Array.Slice.ofBytesBE?Impl]

def ScalarArray.UInt32Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option UInt32Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 4.

Equations

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

def ScalarArray.UInt32Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : UInt32Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 4.

Equations

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

@[simp]

theorem ScalarArray.UInt32Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = UInt32Array.ofBytesBE? b

@[simp]

theorem ScalarArray.UInt32Array.Slice.size_toBytesBE (s : UInt32Array.Slice) : s.toBytesBE.size = 4 * Std.Slice.size s

@[simp]

theorem ScalarArray.UInt32Array.size_toBytesBE (a : UInt32Array) : a.toBytesBE.size = 4 * a.size

@[simp]

theorem ScalarArray.UInt32Array.Slice.getElem_toBytesBE (s : UInt32Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 4] >>> (8 * (3 - j % 4)).toUInt32).toUInt8

@[simp]

theorem ScalarArray.UInt32Array.ofBytesBE?_toBytesBE_slice (s : UInt32Array.Slice) : ofBytesBE? s.toBytesBE = some s.copy

@[simp]

theorem ScalarArray.UInt32Array.ofBytesBE?_toBytesBE (a : UInt32Array) : ofBytesBE? a.toBytesBE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.byteSwapImpl]

def ScalarArray.UInt64Array.byteSwap (a : UInt64Array) : UInt64Array

Reverses the order of the bytes of each element, in place when a is not shared.

Equations

• a.byteSwap = ScalarArray.UInt64Array.mk (Array.map UInt64.byteSwap a.toArray)

@[simp]

theorem ScalarArray.UInt64Array.toArray_byteSwap (a : UInt64Array) : a.byteSwap.toArray = Array.map UInt64.byteSwap a.toArray

@[simp]

theorem ScalarArray.UInt64Array.size_byteSwap (a : UInt64Array) : a.byteSwap.size = a.size

@[simp]

theorem ScalarArray.UInt64Array.getElem_byteSwap (a : UInt64Array) (i : Nat) (h : i < a.byteSwap.size) : a.byteSwap[i] = a[i].byteSwap

@[simp]

theorem ScalarArray.UInt64Array.byteSwap_byteSwap (a : UInt64Array) : a.byteSwap.byteSwap = a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.Slice.toBytesLEImpl]

def ScalarArray.UInt64Array.Slice.toBytesLE (s : UInt64Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (8 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 8] >>> (8 * (j % 8)).toUInt64).toUInt8 }

@[inline]

def ScalarArray.UInt64Array.toBytesLE (a : UInt64Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.ofBytesLE?Impl]

def ScalarArray.UInt64Array.ofBytesLE? (b : ByteArray) : Option UInt64Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 8.

Equations

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

def ScalarArray.UInt64Array.ofBytesLE! (b : ByteArray) : UInt64Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 8.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.Slice.ofBytesLE?Impl]

def ScalarArray.UInt64Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option UInt64Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 8.

Equations

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

def ScalarArray.UInt64Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : UInt64Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 8.

Equations

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

@[simp]

theorem ScalarArray.UInt64Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = UInt64Array.ofBytesLE? b

@[simp]

theorem ScalarArray.UInt64Array.Slice.size_toBytesLE (s : UInt64Array.Slice) : s.toBytesLE.size = 8 * Std.Slice.size s

@[simp]

theorem ScalarArray.UInt64Array.size_toBytesLE (a : UInt64Array) : a.toBytesLE.size = 8 * a.size

@[simp]

theorem ScalarArray.UInt64Array.Slice.getElem_toBytesLE (s : UInt64Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 8] >>> (8 * (j % 8)).toUInt64).toUInt8

@[simp]

theorem ScalarArray.UInt64Array.ofBytesLE?_toBytesLE_slice (s : UInt64Array.Slice) : ofBytesLE? s.toBytesLE = some s.copy

@[simp]

theorem ScalarArray.UInt64Array.ofBytesLE?_toBytesLE (a : UInt64Array) : ofBytesLE? a.toBytesLE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.Slice.toBytesBEImpl]

def ScalarArray.UInt64Array.Slice.toBytesBE (s : UInt64Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (8 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 8] >>> (8 * (7 - j % 8)).toUInt64).toUInt8 }

@[inline]

def ScalarArray.UInt64Array.toBytesBE (a : UInt64Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.ofBytesBE?Impl]

def ScalarArray.UInt64Array.ofBytesBE? (b : ByteArray) : Option UInt64Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 8.

Equations

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

def ScalarArray.UInt64Array.ofBytesBE! (b : ByteArray) : UInt64Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 8.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.UInt64Array.Slice.ofBytesBE?Impl]

def ScalarArray.UInt64Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option UInt64Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 8.

Equations

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

def ScalarArray.UInt64Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : UInt64Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 8.

Equations

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

@[simp]

theorem ScalarArray.UInt64Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = UInt64Array.ofBytesBE? b

@[simp]

theorem ScalarArray.UInt64Array.Slice.size_toBytesBE (s : UInt64Array.Slice) : s.toBytesBE.size = 8 * Std.Slice.size s

@[simp]

theorem ScalarArray.UInt64Array.size_toBytesBE (a : UInt64Array) : a.toBytesBE.size = 8 * a.size

@[simp]

theorem ScalarArray.UInt64Array.Slice.getElem_toBytesBE (s : UInt64Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 8] >>> (8 * (7 - j % 8)).toUInt64).toUInt8

@[simp]

theorem ScalarArray.UInt64Array.ofBytesBE?_toBytesBE_slice (s : UInt64Array.Slice) : ofBytesBE? s.toBytesBE = some s.copy

@[simp]

theorem ScalarArray.UInt64Array.ofBytesBE?_toBytesBE (a : UInt64Array) : ofBytesBE? a.toBytesBE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.byteSwapImpl]

def ScalarArray.Int16Array.byteSwap (a : Int16Array) : Int16Array

Reverses the order of the bytes of each element, in place when a is not shared.

Equations

• a.byteSwap = ScalarArray.Int16Array.mk (Array.map Int16.byteSwap a.toArray)

@[simp]

theorem ScalarArray.Int16Array.toArray_byteSwap (a : Int16Array) : a.byteSwap.toArray = Array.map Int16.byteSwap a.toArray

@[simp]

theorem ScalarArray.Int16Array.size_byteSwap (a : Int16Array) : a.byteSwap.size = a.size

@[simp]

theorem ScalarArray.Int16Array.getElem_byteSwap (a : Int16Array) (i : Nat) (h : i < a.byteSwap.size) : a.byteSwap[i] = a[i].byteSwap

@[simp]

theorem ScalarArray.Int16Array.byteSwap_byteSwap (a : Int16Array) : a.byteSwap.byteSwap = a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.Slice.toBytesLEImpl]

def ScalarArray.Int16Array.Slice.toBytesLE (s : Int16Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (2 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 2].toUInt16 >>> (8 * (j % 2)).toUInt16).toUInt8 }

@[inline]

def ScalarArray.Int16Array.toBytesLE (a : Int16Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.ofBytesLE?Impl]

def ScalarArray.Int16Array.ofBytesLE? (b : ByteArray) : Option Int16Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 2.

Equations

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

def ScalarArray.Int16Array.ofBytesLE! (b : ByteArray) : Int16Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 2.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.Slice.ofBytesLE?Impl]

def ScalarArray.Int16Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option Int16Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 2.

Equations

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

def ScalarArray.Int16Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : Int16Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 2.

Equations

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

@[simp]

theorem ScalarArray.Int16Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = Int16Array.ofBytesLE? b

@[simp]

theorem ScalarArray.Int16Array.Slice.size_toBytesLE (s : Int16Array.Slice) : s.toBytesLE.size = 2 * Std.Slice.size s

@[simp]

theorem ScalarArray.Int16Array.size_toBytesLE (a : Int16Array) : a.toBytesLE.size = 2 * a.size

@[simp]

theorem ScalarArray.Int16Array.Slice.getElem_toBytesLE (s : Int16Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 2].toUInt16 >>> (8 * (j % 2)).toUInt16).toUInt8

@[simp]

theorem ScalarArray.Int16Array.ofBytesLE?_toBytesLE_slice (s : Int16Array.Slice) : ofBytesLE? s.toBytesLE = some s.copy

@[simp]

theorem ScalarArray.Int16Array.ofBytesLE?_toBytesLE (a : Int16Array) : ofBytesLE? a.toBytesLE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.Slice.toBytesBEImpl]

def ScalarArray.Int16Array.Slice.toBytesBE (s : Int16Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (2 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 2].toUInt16 >>> (8 * (1 - j % 2)).toUInt16).toUInt8 }

@[inline]

def ScalarArray.Int16Array.toBytesBE (a : Int16Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.ofBytesBE?Impl]

def ScalarArray.Int16Array.ofBytesBE? (b : ByteArray) : Option Int16Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 2.

Equations

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

def ScalarArray.Int16Array.ofBytesBE! (b : ByteArray) : Int16Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 2.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int16Array.Slice.ofBytesBE?Impl]

def ScalarArray.Int16Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option Int16Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 2.

Equations

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

def ScalarArray.Int16Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : Int16Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 2.

Equations

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

@[simp]

theorem ScalarArray.Int16Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = Int16Array.ofBytesBE? b

@[simp]

theorem ScalarArray.Int16Array.Slice.size_toBytesBE (s : Int16Array.Slice) : s.toBytesBE.size = 2 * Std.Slice.size s

@[simp]

theorem ScalarArray.Int16Array.size_toBytesBE (a : Int16Array) : a.toBytesBE.size = 2 * a.size

@[simp]

theorem ScalarArray.Int16Array.Slice.getElem_toBytesBE (s : Int16Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 2].toUInt16 >>> (8 * (1 - j % 2)).toUInt16).toUInt8

@[simp]

theorem ScalarArray.Int16Array.ofBytesBE?_toBytesBE_slice (s : Int16Array.Slice) : ofBytesBE? s.toBytesBE = some s.copy

@[simp]

theorem ScalarArray.Int16Array.ofBytesBE?_toBytesBE (a : Int16Array) : ofBytesBE? a.toBytesBE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.byteSwapImpl]

def ScalarArray.Int32Array.byteSwap (a : Int32Array) : Int32Array

Reverses the order of the bytes of each element, in place when a is not shared.

Equations

• a.byteSwap = ScalarArray.Int32Array.mk (Array.map Int32.byteSwap a.toArray)

@[simp]

theorem ScalarArray.Int32Array.toArray_byteSwap (a : Int32Array) : a.byteSwap.toArray = Array.map Int32.byteSwap a.toArray

@[simp]

theorem ScalarArray.Int32Array.size_byteSwap (a : Int32Array) : a.byteSwap.size = a.size

@[simp]

theorem ScalarArray.Int32Array.getElem_byteSwap (a : Int32Array) (i : Nat) (h : i < a.byteSwap.size) : a.byteSwap[i] = a[i].byteSwap

@[simp]

theorem ScalarArray.Int32Array.byteSwap_byteSwap (a : Int32Array) : a.byteSwap.byteSwap = a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.Slice.toBytesLEImpl]

def ScalarArray.Int32Array.Slice.toBytesLE (s : Int32Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (4 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 4].toUInt32 >>> (8 * (j % 4)).toUInt32).toUInt8 }

@[inline]

def ScalarArray.Int32Array.toBytesLE (a : Int32Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.ofBytesLE?Impl]

def ScalarArray.Int32Array.ofBytesLE? (b : ByteArray) : Option Int32Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 4.

Equations

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

def ScalarArray.Int32Array.ofBytesLE! (b : ByteArray) : Int32Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 4.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.Slice.ofBytesLE?Impl]

def ScalarArray.Int32Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option Int32Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 4.

Equations

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

def ScalarArray.Int32Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : Int32Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 4.

Equations

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

@[simp]

theorem ScalarArray.Int32Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = Int32Array.ofBytesLE? b

@[simp]

theorem ScalarArray.Int32Array.Slice.size_toBytesLE (s : Int32Array.Slice) : s.toBytesLE.size = 4 * Std.Slice.size s

@[simp]

theorem ScalarArray.Int32Array.size_toBytesLE (a : Int32Array) : a.toBytesLE.size = 4 * a.size

@[simp]

theorem ScalarArray.Int32Array.Slice.getElem_toBytesLE (s : Int32Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 4].toUInt32 >>> (8 * (j % 4)).toUInt32).toUInt8

@[simp]

theorem ScalarArray.Int32Array.ofBytesLE?_toBytesLE_slice (s : Int32Array.Slice) : ofBytesLE? s.toBytesLE = some s.copy

@[simp]

theorem ScalarArray.Int32Array.ofBytesLE?_toBytesLE (a : Int32Array) : ofBytesLE? a.toBytesLE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.Slice.toBytesBEImpl]

def ScalarArray.Int32Array.Slice.toBytesBE (s : Int32Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (4 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 4].toUInt32 >>> (8 * (3 - j % 4)).toUInt32).toUInt8 }

@[inline]

def ScalarArray.Int32Array.toBytesBE (a : Int32Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.ofBytesBE?Impl]

def ScalarArray.Int32Array.ofBytesBE? (b : ByteArray) : Option Int32Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 4.

Equations

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

def ScalarArray.Int32Array.ofBytesBE! (b : ByteArray) : Int32Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 4.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int32Array.Slice.ofBytesBE?Impl]

def ScalarArray.Int32Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option Int32Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 4.

Equations

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

def ScalarArray.Int32Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : Int32Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 4.

Equations

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

@[simp]

theorem ScalarArray.Int32Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = Int32Array.ofBytesBE? b

@[simp]

theorem ScalarArray.Int32Array.Slice.size_toBytesBE (s : Int32Array.Slice) : s.toBytesBE.size = 4 * Std.Slice.size s

@[simp]

theorem ScalarArray.Int32Array.size_toBytesBE (a : Int32Array) : a.toBytesBE.size = 4 * a.size

@[simp]

theorem ScalarArray.Int32Array.Slice.getElem_toBytesBE (s : Int32Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 4].toUInt32 >>> (8 * (3 - j % 4)).toUInt32).toUInt8

@[simp]

theorem ScalarArray.Int32Array.ofBytesBE?_toBytesBE_slice (s : Int32Array.Slice) : ofBytesBE? s.toBytesBE = some s.copy

@[simp]

theorem ScalarArray.Int32Array.ofBytesBE?_toBytesBE (a : Int32Array) : ofBytesBE? a.toBytesBE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.byteSwapImpl]

def ScalarArray.Int64Array.byteSwap (a : Int64Array) : Int64Array

Reverses the order of the bytes of each element, in place when a is not shared.

Equations

• a.byteSwap = ScalarArray.Int64Array.mk (Array.map Int64.byteSwap a.toArray)

@[simp]

theorem ScalarArray.Int64Array.toArray_byteSwap (a : Int64Array) : a.byteSwap.toArray = Array.map Int64.byteSwap a.toArray

@[simp]

theorem ScalarArray.Int64Array.size_byteSwap (a : Int64Array) : a.byteSwap.size = a.size

@[simp]

theorem ScalarArray.Int64Array.getElem_byteSwap (a : Int64Array) (i : Nat) (h : i < a.byteSwap.size) : a.byteSwap[i] = a[i].byteSwap

@[simp]

theorem ScalarArray.Int64Array.byteSwap_byteSwap (a : Int64Array) : a.byteSwap.byteSwap = a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.Slice.toBytesLEImpl]

def ScalarArray.Int64Array.Slice.toBytesLE (s : Int64Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (8 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 8].toUInt64 >>> (8 * (j % 8)).toUInt64).toUInt8 }

@[inline]

def ScalarArray.Int64Array.toBytesLE (a : Int64Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.ofBytesLE?Impl]

def ScalarArray.Int64Array.ofBytesLE? (b : ByteArray) : Option Int64Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 8.

Equations

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

def ScalarArray.Int64Array.ofBytesLE! (b : ByteArray) : Int64Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 8.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.Slice.ofBytesLE?Impl]

def ScalarArray.Int64Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option Int64Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 8.

Equations

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

def ScalarArray.Int64Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : Int64Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 8.

Equations

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

@[simp]

theorem ScalarArray.Int64Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = Int64Array.ofBytesLE? b

@[simp]

theorem ScalarArray.Int64Array.Slice.size_toBytesLE (s : Int64Array.Slice) : s.toBytesLE.size = 8 * Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.size_toBytesLE (a : Int64Array) : a.toBytesLE.size = 8 * a.size

@[simp]

theorem ScalarArray.Int64Array.Slice.getElem_toBytesLE (s : Int64Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 8].toUInt64 >>> (8 * (j % 8)).toUInt64).toUInt8

@[simp]

theorem ScalarArray.Int64Array.ofBytesLE?_toBytesLE_slice (s : Int64Array.Slice) : ofBytesLE? s.toBytesLE = some s.copy

@[simp]

theorem ScalarArray.Int64Array.ofBytesLE?_toBytesLE (a : Int64Array) : ofBytesLE? a.toBytesLE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.Slice.toBytesBEImpl]

def ScalarArray.Int64Array.Slice.toBytesBE (s : Int64Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (8 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 8].toUInt64 >>> (8 * (7 - j % 8)).toUInt64).toUInt8 }

@[inline]

def ScalarArray.Int64Array.toBytesBE (a : Int64Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.ofBytesBE?Impl]

def ScalarArray.Int64Array.ofBytesBE? (b : ByteArray) : Option Int64Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 8.

Equations

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

def ScalarArray.Int64Array.ofBytesBE! (b : ByteArray) : Int64Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 8.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Int64Array.Slice.ofBytesBE?Impl]

def ScalarArray.Int64Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option Int64Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 8.

Equations

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

def ScalarArray.Int64Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : Int64Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 8.

Equations

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

@[simp]

theorem ScalarArray.Int64Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = Int64Array.ofBytesBE? b

@[simp]

theorem ScalarArray.Int64Array.Slice.size_toBytesBE (s : Int64Array.Slice) : s.toBytesBE.size = 8 * Std.Slice.size s

@[simp]

theorem ScalarArray.Int64Array.size_toBytesBE (a : Int64Array) : a.toBytesBE.size = 8 * a.size

@[simp]

theorem ScalarArray.Int64Array.Slice.getElem_toBytesBE (s : Int64Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 8].toUInt64 >>> (8 * (7 - j % 8)).toUInt64).toUInt8

@[simp]

theorem ScalarArray.Int64Array.ofBytesBE?_toBytesBE_slice (s : Int64Array.Slice) : ofBytesBE? s.toBytesBE = some s.copy

@[simp]

theorem ScalarArray.Int64Array.ofBytesBE?_toBytesBE (a : Int64Array) : ofBytesBE? a.toBytesBE = some a

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float32Array.Slice.toBytesLEImpl]

def ScalarArray.Float32Array.Slice.toBytesLE (s : Float32Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (4 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 4].toBits >>> (8 * (j % 4)).toUInt32).toUInt8 }

@[inline]

def ScalarArray.Float32Array.toBytesLE (a : Float32Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float32Array.ofBytesLE?Impl]

def ScalarArray.Float32Array.ofBytesLE? (b : ByteArray) : Option Float32Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 4.

Equations

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

def ScalarArray.Float32Array.ofBytesLE! (b : ByteArray) : Float32Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 4.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float32Array.Slice.ofBytesLE?Impl]

def ScalarArray.Float32Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option Float32Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 4.

Equations

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

def ScalarArray.Float32Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : Float32Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 4.

Equations

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

@[simp]

theorem ScalarArray.Float32Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = Float32Array.ofBytesLE? b

@[simp]

theorem ScalarArray.Float32Array.Slice.size_toBytesLE (s : Float32Array.Slice) : s.toBytesLE.size = 4 * Std.Slice.size s

@[simp]

theorem ScalarArray.Float32Array.size_toBytesLE (a : Float32Array) : a.toBytesLE.size = 4 * a.size

@[simp]

theorem ScalarArray.Float32Array.Slice.getElem_toBytesLE (s : Float32Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 4].toBits >>> (8 * (j % 4)).toUInt32).toUInt8

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float32Array.Slice.toBytesBEImpl]

def ScalarArray.Float32Array.Slice.toBytesBE (s : Float32Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (4 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 4].toBits >>> (8 * (3 - j % 4)).toUInt32).toUInt8 }

@[inline]

def ScalarArray.Float32Array.toBytesBE (a : Float32Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float32Array.ofBytesBE?Impl]

def ScalarArray.Float32Array.ofBytesBE? (b : ByteArray) : Option Float32Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 4.

Equations

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

def ScalarArray.Float32Array.ofBytesBE! (b : ByteArray) : Float32Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 4.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float32Array.Slice.ofBytesBE?Impl]

def ScalarArray.Float32Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option Float32Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 4.

Equations

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

def ScalarArray.Float32Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : Float32Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 4.

Equations

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

@[simp]

theorem ScalarArray.Float32Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = Float32Array.ofBytesBE? b

@[simp]

theorem ScalarArray.Float32Array.Slice.size_toBytesBE (s : Float32Array.Slice) : s.toBytesBE.size = 4 * Std.Slice.size s

@[simp]

theorem ScalarArray.Float32Array.size_toBytesBE (a : Float32Array) : a.toBytesBE.size = 4 * a.size

@[simp]

theorem ScalarArray.Float32Array.Slice.getElem_toBytesBE (s : Float32Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 4].toBits >>> (8 * (3 - j % 4)).toUInt32).toUInt8

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float64Array.Slice.toBytesLEImpl]

def ScalarArray.Float64Array.Slice.toBytesLE (s : Float64Array.Slice) : ByteArray

The elements of s as bytes, each in little-endian order, least significant byte first.

Equations

• s.toBytesLE = { data := Array.ofFn fun (x : Fin (8 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 8].toBits >>> (8 * (j % 8)).toUInt64).toUInt8 }

@[inline]

def ScalarArray.Float64Array.toBytesLE (a : Float64Array) : ByteArray

The elements of a as bytes, each in little-endian order, least significant byte first.

Equations

• a.toBytesLE = a.toSlice.toBytesLE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float64Array.ofBytesLE?Impl]

def ScalarArray.Float64Array.ofBytesLE? (b : ByteArray) : Option Float64Array

Reads b as elements, each in little-endian order, least significant byte first. Returns none if the size of b is not a multiple of 8.

Equations

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

def ScalarArray.Float64Array.ofBytesLE! (b : ByteArray) : Float64Array

Reads b as elements, each in little-endian order, least significant byte first. Panics if the size of b is not a multiple of 8.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float64Array.Slice.ofBytesLE?Impl]

def ScalarArray.Float64Array.Slice.ofBytesLE? (s : UInt8Array.Slice) : Option Float64Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Returns none if the size of s is not a multiple of 8.

Equations

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

def ScalarArray.Float64Array.Slice.ofBytesLE! (s : UInt8Array.Slice) : Float64Array

Reads the bytes of s as elements, each in little-endian order, least significant byte first. Panics if the size of s is not a multiple of 8.

Equations

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

@[simp]

theorem ScalarArray.Float64Array.Slice.ofBytesLE?_toUInt8Array (b : ByteArray) : ofBytesLE? b.toUInt8Array.toSlice = Float64Array.ofBytesLE? b

@[simp]

theorem ScalarArray.Float64Array.Slice.size_toBytesLE (s : Float64Array.Slice) : s.toBytesLE.size = 8 * Std.Slice.size s

@[simp]

theorem ScalarArray.Float64Array.size_toBytesLE (a : Float64Array) : a.toBytesLE.size = 8 * a.size

@[simp]

theorem ScalarArray.Float64Array.Slice.getElem_toBytesLE (s : Float64Array.Slice) (j : Nat) (h : j < s.toBytesLE.size) : s.toBytesLE[j] = (s[j / 8].toBits >>> (8 * (j % 8)).toUInt64).toUInt8

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float64Array.Slice.toBytesBEImpl]

def ScalarArray.Float64Array.Slice.toBytesBE (s : Float64Array.Slice) : ByteArray

The elements of s as bytes, each in big-endian order, most significant byte first.

Equations

• s.toBytesBE = { data := Array.ofFn fun (x : Fin (8 * Std.Slice.size s)) => match x with | ⟨j, hj⟩ => (s[j / 8].toBits >>> (8 * (7 - j % 8)).toUInt64).toUInt8 }

@[inline]

def ScalarArray.Float64Array.toBytesBE (a : Float64Array) : ByteArray

The elements of a as bytes, each in big-endian order, most significant byte first.

Equations

• a.toBytesBE = a.toSlice.toBytesBE

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float64Array.ofBytesBE?Impl]

def ScalarArray.Float64Array.ofBytesBE? (b : ByteArray) : Option Float64Array

Reads b as elements, each in big-endian order, most significant byte first. Returns none if the size of b is not a multiple of 8.

Equations

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

def ScalarArray.Float64Array.ofBytesBE! (b : ByteArray) : Float64Array

Reads b as elements, each in big-endian order, most significant byte first. Panics if the size of b is not a multiple of 8.

Equations

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

@[implemented_by _private.ScalarArray.Bytes.0.ScalarArray.Float64Array.Slice.ofBytesBE?Impl]

def ScalarArray.Float64Array.Slice.ofBytesBE? (s : UInt8Array.Slice) : Option Float64Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Returns none if the size of s is not a multiple of 8.

Equations

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

def ScalarArray.Float64Array.Slice.ofBytesBE! (s : UInt8Array.Slice) : Float64Array

Reads the bytes of s as elements, each in big-endian order, most significant byte first. Panics if the size of s is not a multiple of 8.

Equations

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

@[simp]

theorem ScalarArray.Float64Array.Slice.ofBytesBE?_toUInt8Array (b : ByteArray) : ofBytesBE? b.toUInt8Array.toSlice = Float64Array.ofBytesBE? b

@[simp]

theorem ScalarArray.Float64Array.Slice.size_toBytesBE (s : Float64Array.Slice) : s.toBytesBE.size = 8 * Std.Slice.size s

@[simp]

theorem ScalarArray.Float64Array.size_toBytesBE (a : Float64Array) : a.toBytesBE.size = 8 * a.size

@[simp]

theorem ScalarArray.Float64Array.Slice.getElem_toBytesBE (s : Float64Array.Slice) (j : Nat) (h : j < s.toBytesBE.size) : s.toBytesBE[j] = (s[j / 8].toBits >>> (8 * (7 - j % 8)).toUInt64).toUInt8