TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.Full.Division.Runtime

Native binary64 division runtime #

The normal-result binary64 path performs restoring division on UInt64. Inputs outside the normal-result kernel fall back to the exact generic finite implementation. Correctness proofs are isolated in Division.Proof.

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

Try the common finite division path whose rounded result is normal.

Returning none delegates zeros, subnormals, overflow boundaries, and exceptional encodings to the generic exact-rational implementation.

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

    Use the native normal-result divider when it accepts the operands, otherwise retain the exact generic finite binary64 implementation.

    Instances For