TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Quire.Semantics.Real

Real-valued views of posit quires #

These adapters embed ordinary exact rational quire values into mathlib's Real. They are separate from executable semantics so quire arithmetic does not import real-analysis infrastructure.

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

Complete real semantics obtained by mapping only ordinary exact rational values.

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

    Optional real value of a quire, unavailable exactly for quire NaR.

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

      The zero quire denotes the real number zero.

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

      The NaR quire has no ordinary real interpretation.

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

      The optional real view is unavailable precisely for quire NaR.