Float16 (Half Precision) Array Support

Direct Float16 support using raw byte arrays. No automatic conversions - all conversions must be explicit.

Hardware Requirements:

• ARM: Requires ARMv8.2-A with FP16 vector arithmetic
• x86_64: Requires F16C extension (Ivy Bridge+)
• Returns error if hardware support is unavailable

Performance Benefits:

• 4x memory savings vs Float64, 2x vs Float32
• SIMD width: NEON 8 halfs/op, AVX2+F16C 8 halfs/op
• Direct GPU tensor interop without conversion

structure Hesper.Float16.Float16Array : Type

Float16 array stored as raw bytes (2 bytes per element). Works directly with C FFI and GPU 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 (2 bytes per float16)

• numElements : Nat

  Number of Float16 elements (NOT bytes)

def Hesper.Float16.instInhabitedFloat16Array.default : Float16Array

Equations

• Hesper.Float16.instInhabitedFloat16Array.default = { data := default, numElements := default }

instance Hesper.Float16.instInhabitedFloat16Array : Inhabited Float16Array

Equations

• Hesper.Float16.instInhabitedFloat16Array = { default := Hesper.Float16.instInhabitedFloat16Array.default }

def Hesper.Float16.size (arr : Float16Array) : Nat

Get number of Float16 elements

Equations

• Hesper.Float16.size arr = arr.numElements

def Hesper.Float16.empty : Float16Array

Create empty Float16Array

Equations

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

def Hesper.Float16.fromBytes (bytes : ByteArray) : Option Float16Array

Create Float16Array from raw ByteArray (must be 2-byte aligned)

Equations

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

@[extern lean_f16_hw_check]

opaque Hesper.Float16.hasHardwareSupport : IO Bool

Check if FP16 hardware support is available

def Hesper.Float16.simdAdd (a b : Float16Array) : IO Float16Array

Equations

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

@[extern lean_f16_from_f64_array]

opaque Hesper.Float16.fromFloatArray (arr : FloatArray) : IO Float16Array

ONLY for explicit conversion when needed - converts Float64 to Float16

@[extern lean_f16_to_f64_array]

opaque Hesper.Float16.toFloatArray (arr : Float16Array) : IO FloatArray

ONLY for explicit conversion when needed - converts Float16 to Float64

@[extern lean_f16_get]

opaque Hesper.Float16.get (arr : Float16Array) (i : USize) : IO Float

Get single element (converts to Float64 only for access)

@[extern lean_f16_set]

opaque Hesper.Float16.set (arr : Float16Array) (i : USize) (val : Float) : IO Float16Array

Set single element (converts from Float64)

def Hesper.Float16.toString (arr : Float16Array) : IO String

Equations

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