def Float.Model.UnpackedFloat.neg : UnpackedFloat → UnpackedFloat

Negates the given float.

Equations

• Float.Model.UnpackedFloat.notANumber.neg = Float.Model.UnpackedFloat.notANumber
• (Float.Model.UnpackedFloat.infinity s).neg = Float.Model.UnpackedFloat.infinity (-s)
• (Float.Model.UnpackedFloat.zero s).neg = Float.Model.UnpackedFloat.zero (-s)
• (Float.Model.UnpackedFloat.finite s m e hm).neg = Float.Model.UnpackedFloat.finite (-s) m e hm

def Float.Model.UnpackedFloat.abs : UnpackedFloat → UnpackedFloat

Returns the given float with positive sign.

Equations

• Float.Model.UnpackedFloat.notANumber.abs = Float.Model.UnpackedFloat.notANumber
• (Float.Model.UnpackedFloat.infinity s).abs = Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive
• (Float.Model.UnpackedFloat.zero s).abs = Float.Model.UnpackedFloat.zero Float.Model.UnpackedFloat.Sign.positive
• (Float.Model.UnpackedFloat.finite s m e hm).abs = Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive m e hm