TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Semantics.Real

Optional real-valued semantics of posits #

The exact rational meaning of every ordinary posit embeds into mathlib's Real. NaR remains ExceptionalValue.notAReal in the complete view and none in the partial view.

Posit.Semantics.Exact.Runtime provides the executable rational denotation. This module adds real coordinates for proofs.

source
@[inline]
noncomputable def FloatLib.Floats.Formats.Posit.Model.ExactValue.toRealValue {format : Format} (value : ExactValue format) :
Numerics.NumericalValue ℝ

Canonically embed finite rational meanings into mathlib reals.

Instances For
    source
    @[inline]
    noncomputable def FloatLib.Floats.Formats.Posit.Model.decodeReal {format : Format} (value : Model format) :
    Numerics.NumericalValue ℝ

    Complete real-valued view, obtained only by mapping finite rational values.

    Instances For
      source
      @[inline]
      noncomputable def FloatLib.Floats.Formats.Posit.Model.toReal? {format : Format} (value : Model format) :
      Option ℝ

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

      Instances For
        source
        @[simp]
        theorem FloatLib.Floats.Formats.Posit.Model.toReal?_zero (format : Format) :
        (zero format).toReal? = some 0

        The canonical posit zero denotes real zero.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.Posit.Model.toReal?_nar (format : Format) :
        (nar format).toReal? = none

        Posit NaR has no ordinary real interpretation.

        source
        theorem FloatLib.Floats.Formats.Posit.Model.toReal?_eq_none_iff {format : Format} (value : Model format) :
        value.toReal? = none ↔ value.isNaR = true

        The optional real view is unavailable precisely for the unique NaR word.