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

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

Assumes num < den.

Equations

• Float.Model.UnpackedFloat.accuracyOfFraction num den = if num = 0 then Float.Model.UnpackedFloat.Accuracy.exact else Float.Model.UnpackedFloat.Accuracy.inexact (compare (2 * 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.

Equations

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

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.

Equations

• One or more equations did not get rendered due to their size.
• Float.Model.UnpackedFloat.div spec Float.Model.UnpackedFloat.notANumber x✝ = Float.Model.UnpackedFloat.notANumber
• Float.Model.UnpackedFloat.div spec x✝ Float.Model.UnpackedFloat.notANumber = Float.Model.UnpackedFloat.notANumber
• Float.Model.UnpackedFloat.div spec (Float.Model.UnpackedFloat.infinity sign) (Float.Model.UnpackedFloat.infinity sign_1) = Float.Model.UnpackedFloat.notANumber
• Float.Model.UnpackedFloat.div spec (Float.Model.UnpackedFloat.infinity sign₁) (Float.Model.UnpackedFloat.zero sign₂) = Float.Model.UnpackedFloat.infinity (sign₁ / sign₂)
• Float.Model.UnpackedFloat.div spec (Float.Model.UnpackedFloat.zero sign₁) (Float.Model.UnpackedFloat.infinity sign₂) = Float.Model.UnpackedFloat.zero (sign₁ / sign₂)
• Float.Model.UnpackedFloat.div spec (Float.Model.UnpackedFloat.zero sign) (Float.Model.UnpackedFloat.zero sign_1) = Float.Model.UnpackedFloat.notANumber