Division specification

This exact-rational reference operation defines the proof target for every validated FloatFormat.

Finite operands with a nonzero divisor are divided as an exact scaled rational and rounded to nearest with ties to even. Special operands and division by zero follow the descriptor's encoding policy. This module defines the value-only reference operation; explicit rounding directions and status flags belong to the separate directed and status APIs. Word and arbitrary-width division kernels refine this same reference definition.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Spec.divSpecial {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Division result when at least one operand is non-finite.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Spec.div {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Exact rational division followed by nearest-even rounding in the destination descriptor.