def div_impl {e s : Nat} (a b : PackedFloat e s) (mode : RoundingMode) : PackedFloat e s

Equations

• One or more equations did not get rendered due to their size.

def div {e s : Nat} (a b : PackedFloat e s) (mode : RoundingMode) : PackedFloat e s

Division of two floating-point numbers, rounded to a floating point number using the provided rounding mode.

Equations

• One or more equations did not get rendered due to their size.