TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec

Reference operations for binary descriptors #

These definitions lift the binary model specifications through the representation-preserving descriptor codec. Executable backend implementations and their refinement proofs live separately in Descriptor.Backends.

source
def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec.add {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
ExecFloat (Descriptor format)

Descriptor-aware reference addition.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec.sub {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
    ExecFloat (Descriptor format)

    Descriptor-aware reference subtraction.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec.mul {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
      ExecFloat (Descriptor format)

      Descriptor-aware reference multiplication.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec.div {format : FloatFormat} (left right : ExecFloat (Descriptor format)) :
        ExecFloat (Descriptor format)

        Descriptor-aware reference division.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec.sqrt {format : FloatFormat} (value : ExecFloat (Descriptor format)) :
          ExecFloat (Descriptor format)

          Descriptor-aware reference square root.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Spec.fma {format : FloatFormat} (left right third : ExecFloat (Descriptor format)) :
            ExecFloat (Descriptor format)

            Descriptor-aware reference fused multiply-add.

            Instances For