Low-level rational rounding primitives #
Format-independent executable quotient operations support nearest-even and directed rational
rounding. The quotient layer stays below Model.Arithmetic, so native arithmetic kernels can
reuse its proofs without an import cycle through the public dispatcher. The ceiling
of a quotient is Numerics.roundQuotient .up, shared with every other quotient rounder.
@[inline]
def
FloatLib.Floats.Formats.BinaryInterchange.Model.roundQuotDirected
(roundUp : Bool)
(numerator denominator : ℕ)
:
Round a nonnegative quotient to an integer, selecting floor or ceiling.