TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Arithmetic.Runtime

Format-parameterized binary arithmetic runtime #

The six model operations use the structural dispatchers selected for a validated format descriptor. This module contains only executable definitions; their refinement theorems live in Arithmetic.Proof.

source
def FloatLib.Floats.Formats.BinaryInterchange.Model.add {fmt : FloatFormat} (x y : Model fmt) :
Model fmt

Automatically dispatched addition for any validated format descriptor.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.sub {fmt : FloatFormat} (x y : Model fmt) :
    Model fmt

    Automatically dispatched subtraction for any validated format descriptor.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Model.mul {fmt : FloatFormat} (x y : Model fmt) :
      Model fmt

      Automatically dispatched multiplication for any validated format descriptor.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Model.div {fmt : FloatFormat} (x y : Model fmt) :
        Model fmt

        Automatically dispatched division for any validated format descriptor.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt {fmt : FloatFormat} (x : Model fmt) :
          Model fmt

          Automatically dispatched square root for any validated format descriptor.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Model.fma {fmt : FloatFormat} (x y z : Model fmt) :
            Model fmt

            Automatically dispatched fused multiply-add for any validated format descriptor.

            Instances For