TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Narrow.Addition.Runtime

Native-word addition for generic binary32 #

The nonzero finite path extracts fields and packs the result with UInt32 and UInt64. Both entry points return none when either operand is a NaN or infinity, and the caller applies the IEEE policy for those. Addition.Proof has the proofs.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.addFinite? (x y : Value) :
Option Value

Finite binary32 addition through exact dyadic coordinates.

It returns none when an operand is a NaN or infinity.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.addFiniteWord? (x y : Value) :
    Option Value

    Machine-word implementation of finite binary32 addition.

    When the exponent gap is at most 39, both aligned significands and their sum fit in one UInt64. At larger gaps the smaller finite significand is strictly below half an ulp, so nearest-even rounding returns the dominant operand.

    Instances For