Float32 Array Support

Direct Float32 (single precision) support using raw byte arrays. No automatic conversions - all conversions must be explicit.

Performance Benefits:

• 2x memory savings vs Float64
• SIMD width: AVX2 8 vs 4, NEON 4 vs 2
• Direct GPU/FFI interop without conversion overhead

structure Hesper.Float32.Float32Array : Type

Float32 array stored as raw bytes (4 bytes per element). Works directly with C FFI without type conversion overhead.

IMPORTANT: We store numElements explicitly because Lean cannot properly access ByteArray.size when the ByteArray is wrapped in a struct from C++.

• data : ByteArray

  Raw byte representation (4 bytes per float32)

• numElements : Nat

  Number of Float32 elements (NOT bytes)

instance Hesper.Float32.instInhabitedFloat32Array : Inhabited Float32Array

Equations

• Hesper.Float32.instInhabitedFloat32Array = { default := Hesper.Float32.instInhabitedFloat32Array.default }

def Hesper.Float32.instInhabitedFloat32Array.default : Float32Array

Equations

• Hesper.Float32.instInhabitedFloat32Array.default = { data := default, numElements := default }

def Hesper.Float32.size (arr : Float32Array) : Nat

Get number of Float32 elements

Equations

• Hesper.Float32.size arr = arr.numElements

def Hesper.Float32.empty : Float32Array

Create empty Float32Array

Equations

• Hesper.Float32.empty = { data := ByteArray.empty, numElements := 0 }

def Hesper.Float32.fromBytes (bytes : ByteArray) : Option Float32Array

Create Float32Array from raw ByteArray (must be 4-byte aligned)

Equations

• Hesper.Float32.fromBytes bytes = if (bytes.size % 4 == 0) = true then some { data := bytes, numElements := bytes.size / 4 } else none

def Hesper.Float32.simdAdd (a b : Float32Array) : Float32Array

Equations

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

@[extern lean_f32_from_f64_array]

opaque Hesper.Float32.fromFloatArray (arr : FloatArray) : Float32Array

ONLY for explicit conversion when needed - converts Float64 to Float32

@[extern lean_f32_to_f64_array]

opaque Hesper.Float32.toFloatArray (arr : Float32Array) : FloatArray

ONLY for explicit conversion when needed - converts Float32 to Float64

@[extern lean_f32_get]

opaque Hesper.Float32.get (arr : Float32Array) (i : USize) : Float

Get single element (converts to Float64 only for access)

@[extern lean_f32_set]

opaque Hesper.Float32.set (arr : Float32Array) (i : USize) (val : Float) : Float32Array

Set single element (converts from Float64)

instance Hesper.Float32.instToStringFloat32Array : ToString Float32Array

Equations

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