TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Real

Optional real-valued views of configured posits #

This adapter embeds the exact rational value of an ordinary configured posit into mathlib's Real. The optional view returns none for NaR; the complete view retains its exceptional status.

source
@[inline]
noncomputable def FloatLib.Floats.ExecFloat.Posit.decodeReal {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
Numerics.NumericalValue ℝ

Complete real-valued view of the exact rational semantics.

Instances For
    source
    @[inline]
    noncomputable def FloatLib.Floats.ExecFloat.Posit.toReal? {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
    Option ℝ

    Exact real value of an ordinary configured posit, or none exactly for NaR.

    Instances For
      source
      @[simp]
      theorem FloatLib.Floats.ExecFloat.Posit.toReal?_eq_none_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
      toReal? value = none ↔ isNaR value = true

      The public optional real view is absent precisely for the unique NaR value.