TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.Instances

Ordinary interfaces and exact conversion for static-byte formats #

Every nominal static-byte family uses the same descriptor-level rules for literals, negation, comparison, and display. Defining those instances here keeps standards packages focused on their encodings and kernels instead of repeating adapters around the binary proof model.

Natural and decimal literals are rounded once from exact rationals; they never pass through a host floating-point value. This module also installs the exact decoder, explicit-policy quantizer, and default quantization context shared by these families.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.instFormatDisplay {F : Type u} [Family F] :
ExecFloat.FormatDisplay F

Print the mathematical binary value rather than the compact byte carrier.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.instComparison {F : Type u} [Family F] :
ExecFloat.Comparison F

Compare through the exact-width binary model.

NaNs remain unordered, signed zeros compare equal, and finite-only descriptors inherit the same descriptor-generic rule without a format-specific comparison implementation.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.instOfNatExecFloat {F : Type u} [Family F] (value : ℕ) :
OfNat (ExecFloat F) value

Round a natural literal once, to nearest with ties to even, in the destination descriptor.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.instOfScientificExecFloat {F : Type u} [Family F] :
OfScientific (ExecFloat F)

Round a decimal or scientific literal once from its exact rational value.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.instNegExecFloat {F : Type u} [Family F] :
Neg (ExecFloat F)

Negate the proof-model value and repack it into the same direct byte carrier.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.quantizer {F : Type u} [Family F] :
ExecFloat.Quantizer (ExecFloat F) Numerics.SignedRat

Every nominal static-byte binary destination uses the shared explicit binary policy.

source
@[instance_reducible]
instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.defaultQuantizer {F : Type u} [Family F] :
ExecFloat.DefaultQuantizer (ExecFloat F) Numerics.SignedRat

Context-free conversion uses the canonical binary conversion context.