def Float.Model.UnpackedFloat.accuracyOfFraction (num den : Nat) : Accuracy

Returns the accuracy corresponding to the point y + (num/den)ulp.

Assumes num < den.

def Float.Model.UnpackedFloat.divCore (spec : Format) (m₁ : Nat) (e₁ : Int) (m₂ : Nat) (e₂ : Int) : Nat × Int × Accuracy

Computes a (mantissa, exponent) pair for the quotient with enough bits to populate the mantissa for the given specification. Also returns an Accuracy stating how the returned pair relates to the infinitely precise quotient.

def Float.Model.UnpackedFloat.div (spec : Format) : UnpackedFloat → UnpackedFloat → UnpackedFloat

Computes the quotient of two floating point numbers and rounds the result according to the given specification.