TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Configured.Plan

Execution planning for exact fixed-point arithmetic #

The direct integer-coefficient operations are both the executable implementations and their reference specifications.

Same-scale addition and subtraction need no rounding. This plan registers their direct implementations with ExecFloat; rational exactness is proved separately in Configured.Proof. Conversions and scale-composing multiplication use their own APIs.

source
def FloatLib.Floats.ExecFloat.FixedPoint.Plan.estimate (operation : Backend.Operation) :
Backend.Candidate

Cost description of direct unbounded-integer coefficient arithmetic.

Instances For
    source
    def FloatLib.Floats.ExecFloat.FixedPoint.Plan.addCertified {radix : Numerics.Radix} {fractionalDigits : ℕ} :
    Backend.Certified add

    Certified exact same-scale addition.

    Instances For
      source
      def FloatLib.Floats.ExecFloat.FixedPoint.Plan.subCertified {radix : Numerics.Radix} {fractionalDigits : ℕ} :
      Backend.Certified sub

      Certified exact same-scale subtraction.

      Instances For