Documentation

LeanMlir.LEBytes

Little-endian packing for the FFI buffers #

Every buffer the runtimes read — shape descriptors, labels, token ids, anchor priors, f32 tensors — is 4-byte little-endian. These are the two writers; the reader is F32.readLabel. Import-free, so the pure-data ParamLayouts can use them.

@[inline]

def pushU32LE (acc : ByteArray) (v : Nat) :

Append v mod 2³² as 4 little-endian bytes (an int32 / uint32 record).

Equations

pushU32LE acc v = (((acc.push (v.toUInt32 &&& 255).toUInt8).push (v.toUInt32 >>> 8 &&& 255).toUInt8).push (v.toUInt32 >>> 16 &&& 255).toUInt8).push (v.toUInt32 >>> 24 &&& 255).toUInt8

Instances For

@[inline]

def pushF32LE (acc : ByteArray) (x : Float) :

Append x as 4 little-endian f32 bytes (narrowing f64 → Float32).

Equations

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

Instances For