TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Instances

Comparison, display, and literal instances for configured posits #

Numerical literals are rounded once from exact rationals. Display and comparison operate on the exact-width model independently of the selected packed carrier.

source
@[instance_reducible]
instance FloatLib.Floats.ExecFloat.Posit.instFormatDisplayFamily {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] :
FormatDisplay (Formats.Posit.Configured.Family format code plan)

Configured posits print their mathematical value rather than their packed carrier.

source
@[instance_reducible]
instance FloatLib.Floats.ExecFloat.Posit.configuredComparison {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [codec : ModelCodec plan (Formats.Posit.Model format) code] :
Comparison (Formats.Posit.Configured.Family format code plan)

Configured posit comparison follows the standard's total signed-word order.

NaR compares below every real posit because the standard compares complete words as signed two's-complement integers; this does not give NaR a real or infinite numerical meaning.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.Posit.instOfNatExecFloatFamilyOfModelCodecStoragePlanModel {format : Format} {plan : Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ℕ) :
OfNat (ExecFloat (Configured.Family format code plan)) value

Natural literals are rounded once from their exact value into the destination posit.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.Posit.instOfScientificExecFloatFamilyOfModelCodecStoragePlanModel {format : Format} {plan : Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] :
OfScientific (ExecFloat (Configured.Family format code plan))

Decimal literals are rounded once from an exact rational, never through a host float.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.Posit.instNegExecFloatFamilyOfModelCodecStoragePlanModel {format : Format} {plan : Configured.StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] :
Neg (ExecFloat (Configured.Family format code plan))

Posit negation is whole-word two's complement and fixes zero and NaR.