TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Quire.Configured.Views

Optional mathematical views of configured posit quires #

These wrappers expose real and projective-line denotations through the configured API. They are kept outside Configured.Runtime because executable rational quire arithmetic does not require classical real-number or projective-geometry dependencies.

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

Complete real quire semantics obtained from the exact rational denotation.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Posit.Quire.toProjectiveRatLine {format : Formats.Posit.Format} (value : Formats.Posit.Quire.Model format) :
    Projectivization ℚ (Fin 2 → ℚ)

    Mathlib rational projective-line view of a configured quire.

    Instances For
      source
      @[inline]
      noncomputable def FloatLib.Floats.ExecFloat.Posit.Quire.toProjectiveRealLine {format : Formats.Posit.Format} (value : Formats.Posit.Quire.Model format) :
      Projectivization ℝ (Fin 2 → ℝ)

      Mathlib real projective-line view of a configured quire.

      Instances For