Literal and dispatch instances for exact fixed point #
Literals use exact integer embedding or one rational ties-to-even rounding step. Same-scale addition and subtraction dispatch to their certified direct kernels.
@[instance_reducible]
instance
FloatLib.Floats.ExecFloat.FixedPoint.instNeg
{radix : Numerics.Radix}
{fractionalDigits : ℕ}
:
Neg (FixedPoint radix fractionalDigits)
@[instance_reducible]
instance
FloatLib.Floats.ExecFloat.FixedPoint.instOfNat
{radix : Numerics.Radix}
{fractionalDigits : ℕ}
(value : ℕ)
:
OfNat (FixedPoint radix fractionalDigits) value
Natural literals are embedded exactly into the configured fixed-point grid.
@[instance_reducible]
instance
FloatLib.Floats.ExecFloat.FixedPoint.instOfScientific
{radix : Numerics.Radix}
{fractionalDigits : ℕ}
:
OfScientific (FixedPoint radix fractionalDigits)
Decimal and scientific literals are rounded once from an exact rational to nearest, ties to even.
@[instance_reducible, always_inline]
instance
FloatLib.Floats.ExecFloat.FixedPoint.instAddFamily
{radix : Numerics.Radix}
{fractionalDigits : ℕ}
[planning : Backend.PolicyFor (Family radix fractionalDigits)]
:
Same-scale fixed-point addition participates in ordinary ExecFloat dispatch.
@[instance_reducible, always_inline]
instance
FloatLib.Floats.ExecFloat.FixedPoint.instSubFamily
{radix : Numerics.Radix}
{fractionalDigits : ℕ}
[planning : Backend.PolicyFor (Family radix fractionalDigits)]
:
Same-scale fixed-point subtraction participates in ordinary ExecFloat dispatch.