TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Semantics.Ordinary.Real

Real coordinates for ordinary posits #

An ordinary posit excludes NaR and therefore has a total exact rational coordinate. This module canonically embeds that coordinate into mathlib's Real for use in proofs.

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

Canonical exact-real coordinate obtained from the ordinary rational semantics.

Instances For
    source
    @[simp]
    theorem FloatLib.Floats.Formats.Posit.Model.Ordinary.model_toReal?_eq_some {format : Format} (value : Ordinary format) :
    (↑value).toReal? = some value.toReal

    The model's optional real view agrees with the total ordinary real coordinate.

    source
    @[simp]
    theorem FloatLib.Floats.Formats.Posit.Model.Ordinary.toReal_zero (format : Format) :
    (zero format).toReal = 0

    Ordinary posit zero denotes real zero.