Computes the product 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.mul spec Float.Model.UnpackedFloat.notANumber x✝ = Float.Model.UnpackedFloat.notANumber
- Float.Model.UnpackedFloat.mul spec x✝ Float.Model.UnpackedFloat.notANumber = Float.Model.UnpackedFloat.notANumber
- Float.Model.UnpackedFloat.mul spec (Float.Model.UnpackedFloat.infinity sign₁) (Float.Model.UnpackedFloat.infinity sign₂) = Float.Model.UnpackedFloat.infinity (sign₁ * sign₂)
- Float.Model.UnpackedFloat.mul spec (Float.Model.UnpackedFloat.infinity sign) (Float.Model.UnpackedFloat.zero sign_1) = Float.Model.UnpackedFloat.notANumber
- Float.Model.UnpackedFloat.mul spec (Float.Model.UnpackedFloat.zero sign) (Float.Model.UnpackedFloat.infinity sign_1) = Float.Model.UnpackedFloat.notANumber
- Float.Model.UnpackedFloat.mul spec (Float.Model.UnpackedFloat.zero sign₁) (Float.Model.UnpackedFloat.zero sign₂) = Float.Model.UnpackedFloat.zero (sign₁ * sign₂)