TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Operations.Classification.Runtime

Binary classification and canonicality queries #

The non-signaling queries of IEEE 754-2019 §5.7.2 inspect the complete descriptor. They also apply to custom biases and finite encodings: an all-ones exponent can be normal, and the FNUZ negative-zero word is a quiet NaN.

Every word in these implicit-leading-bit layouts is a canonical interchange encoding. This includes every NaN payload; canonicality does not mean choosing the library's preferred NaN or repacking through Lean's logical model.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.isNormal {fmt : FloatFormat} (x : Model fmt) :
Bool

A normal value is finite and has a nonzero biased exponent field.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.classify {fmt : FloatFormat} (x : Model fmt) :
    Numerics.IEEEClass

    Classify without quieting NaNs or raising exceptions, using the complete descriptor.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.Formats.BinaryInterchange.Model.isCanonical {fmt : FloatFormat} :
      Model fmt → Bool

      Every exact-width word of an implicit-leading-bit binary layout is canonical.

      Instances For