Documentation

ScalarArray.Conversions

Conversions to and from core's scalar arrays #

UInt8Array and core's ByteArray have the same runtime representation, a scalar array with element size 1, and so do Float64Array and core's FloatArray, with element size 8. The conversions between them are the identity at runtime, so they never copy.

source
@[implemented_by _private.ScalarArray.Conversions.0.ScalarArray.UInt8Array.toByteArrayImpl]
def ScalarArray.UInt8Array.toByteArray (a : UInt8Array) :
ByteArray

The same array as a ByteArray, without copying.

Equations
Instances For
    source
    @[implemented_by _private.ScalarArray.Conversions.0.ScalarArray.UInt8Array.ofByteArrayImpl]
    def ScalarArray.UInt8Array.ofByteArray (b : ByteArray) :
    UInt8Array

    The same array as a UInt8Array, without copying.

    Equations
    Instances For
      source
      @[simp]
      theorem ScalarArray.UInt8Array.data_toByteArray (a : UInt8Array) :
      a.toByteArray.data = a.toArray
      source
      @[simp]
      theorem ScalarArray.UInt8Array.toArray_ofByteArray (b : ByteArray) :
      (ofByteArray b).toArray = b.data
      source
      @[simp]
      theorem ScalarArray.UInt8Array.size_toByteArray (a : UInt8Array) :
      a.toByteArray.size = a.size
      source
      @[simp]
      theorem ScalarArray.UInt8Array.size_ofByteArray (b : ByteArray) :
      (ofByteArray b).size = b.size
      source
      @[simp]
      theorem ScalarArray.UInt8Array.getElem_ofByteArray (b : ByteArray) (i : Nat) (h : i < (ofByteArray b).size) :
      (ofByteArray b)[i] = b[i]
      source
      @[simp]
      theorem ScalarArray.UInt8Array.ofByteArray_toByteArray (a : UInt8Array) :
      ofByteArray a.toByteArray = a
      source
      @[simp]
      theorem ScalarArray.UInt8Array.toByteArray_ofByteArray (b : ByteArray) :
      (ofByteArray b).toByteArray = b
      source
      @[implemented_by _private.ScalarArray.Conversions.0.ScalarArray.Float64Array.toFloatArrayImpl]
      def ScalarArray.Float64Array.toFloatArray (a : Float64Array) :
      FloatArray

      The same array as a FloatArray, without copying.

      Equations
      Instances For
        source
        @[implemented_by _private.ScalarArray.Conversions.0.ScalarArray.Float64Array.ofFloatArrayImpl]
        def ScalarArray.Float64Array.ofFloatArray (b : FloatArray) :
        Float64Array

        The same array as a Float64Array, without copying.

        Equations
        Instances For
          source
          @[simp]
          theorem ScalarArray.Float64Array.data_toFloatArray (a : Float64Array) :
          a.toFloatArray.data = a.toArray
          source
          @[simp]
          theorem ScalarArray.Float64Array.toArray_ofFloatArray (b : FloatArray) :
          (ofFloatArray b).toArray = b.data
          source
          @[simp]
          theorem ScalarArray.Float64Array.ofFloatArray_toFloatArray (a : Float64Array) :
          ofFloatArray a.toFloatArray = a
          source
          @[simp]
          theorem ScalarArray.Float64Array.toFloatArray_ofFloatArray (b : FloatArray) :
          (ofFloatArray b).toFloatArray = b
          source
          @[inline]
          def ByteArray.toUInt8Array (b : ByteArray) :
          ScalarArray.UInt8Array

          The same array as a UInt8Array, without copying.

          Equations
          Instances For
            source
            @[simp]
            theorem ByteArray.size_toUInt8Array (b : ByteArray) :
            b.toUInt8Array.size = b.size
            source
            @[simp]
            theorem ByteArray.getElem_toUInt8Array (b : ByteArray) (i : Nat) (h : i < b.toUInt8Array.size) :
            b.toUInt8Array[i] = b[i]
            source
            @[inline]
            def FloatArray.toFloat64Array (b : FloatArray) :
            ScalarArray.Float64Array

            The same array as a Float64Array, without copying.

            Equations
            Instances For