TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Generic.AddDyadic.Runtime

Executable signed-magnitude dyadic addition #

Exact dyadic addition uses separate signs and natural-number magnitudes. Correctness proofs and the compiler substitution live in AddDyadic.Proof.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadicMagnitudes (leftSign rightSign : Bool) (left right : ℕ) (exponent : ℤ) :
Numerics.Dyadic

Add two nonzero signed magnitudes at a shared dyadic exponent.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.addDyadicImpl (a b : Numerics.Dyadic) :
    Numerics.Dyadic

    Exact dyadic addition using separate signs and natural-number magnitudes.

    Zero operands are handled before alignment. For two nonzero operands, the significand with the larger exponent is shifted to the smaller exponent before the magnitudes are combined. No rounding occurs here.

    Instances For