Executable exact rational semantics of posits

Every ordinary posit word denotes an exact rational. The unique NaR word denotes ExceptionalValue.notAReal and has no partial rational value.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.ExactValue.forget {format : Format} : ExactValue format → Numerics.NumericalValue ℚ

Forget tapered field metadata into the common exact rational value domain.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.ExactValue.toRat? {format : Format} : ExactValue format → Option ℚ

Recover the exact rational value of an ordinary decoded value; NaR returns none.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.decode {format : Format} (value : Model format) : Numerics.NumericalValue ℚ

Complete exact rational semantics of every posit word.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.toRat? {format : Format} (value : Model format) : Option ℚ

Exact rational represented by an ordinary word, or none exactly for NaR.