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. With those instances defined here, standards packages need not repeat adapters around the binary proof model.

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

@[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.

@[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 are unordered, signed zeros compare equal, and finite-only descriptors inherit the same descriptor-generic rule without a format-specific comparison implementation.

@[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.

@[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.

@[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.

@[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 binary conversion policy.

@[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.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.roundingModes {F : Type u} [Family F] : ExecFloat.RoundingModes (ExecFloat F) Model.IEEERoundingMode

Conversions into a static-byte destination take an IEEERoundingMode, nearest by default.

@[instance_reducible, inline]

instance FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.modeContext {F : Type u} [Family F] (mode : Model.IEEERoundingMode) : ExecFloat.ModeContext (ExecFloat F) Numerics.SignedRat mode

A conversion's (mode := m) selects the canonical binary context rounding in direction m, and .nearest the canonical context itself.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.StaticByte.Conversion.context_modeContext {F : Type u} [Family F] (mode : Model.IEEERoundingMode) : ExecFloat.ModeContext.context = ExecFloat.Binary.Conversion.Context.withRounding mode

The context a static-byte conversion's (mode := m) selects is Context.withRounding m.