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

Computes the difference 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.sub spec Float.Model.UnpackedFloat.notANumber x✝ = Float.Model.UnpackedFloat.notANumber
• Float.Model.UnpackedFloat.sub spec x✝ Float.Model.UnpackedFloat.notANumber = Float.Model.UnpackedFloat.notANumber
• Float.Model.UnpackedFloat.sub spec (Float.Model.UnpackedFloat.infinity s) x✝ = Float.Model.UnpackedFloat.infinity s
• Float.Model.UnpackedFloat.sub spec x✝ (Float.Model.UnpackedFloat.infinity s) = Float.Model.UnpackedFloat.infinity (-s)
• Float.Model.UnpackedFloat.sub spec x✝ (Float.Model.UnpackedFloat.zero sign) = x✝