TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Interval

Outward rounding for configured posit endpoints #

This adapter uses the same candidate search as model-level posit intervals, packing each endpoint through the existing storage codec. It applies to every configured width and storage plan, so callers can use ExecFloat.Posit directly with the common interval operations. The exact decoded check rejects NaR and overflow just as it does for model endpoints.

source
@[reducible, inline]
abbrev FloatLib.Floats.ExecFloat.Posit.Interval {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} :
Type

An interval over the configured posit carrier, independent of its storage representation.

Instances For
    source
    def FloatLib.Floats.ExecFloat.Posit.intervalRounding {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
    Numerics.OutwardRounding (ExecFloat (Formats.Posit.Configured.Family format code plan)) ℚ

    Outward rounding through the posit storage codec, with explicit finite-range failure.

    Instances For
      source
      theorem FloatLib.Floats.ExecFloat.Posit.intervalRounding_enclose? {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x : ℚ) :
      intervalRounding.enclose? x = Option.map (Numerics.Interval.map ofModel) ((Formats.Posit.intervalRounding format).enclose? x)

      Changing the storage codec preserves success, failure, and both model endpoints.