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

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