def Float.Model.UnpackedFloat.isFinite : UnpackedFloat → Bool

Returns true if the float represents a real number, i.e., it is neither infinite nor NaN.

Equations

• Float.Model.UnpackedFloat.notANumber.isFinite = false
• (Float.Model.UnpackedFloat.infinity sign).isFinite = false
• (Float.Model.UnpackedFloat.zero sign).isFinite = true
• (Float.Model.UnpackedFloat.finite sign mantissa exponent mantissa_pos).isFinite = true

def Float.Model.UnpackedFloat.isInf : UnpackedFloat → Bool

Returns true if the float is positive or negative infinity.

Equations

• (Float.Model.UnpackedFloat.infinity sign).isInf = true
• x✝.isInf = false

def Float.Model.UnpackedFloat.isNaN : UnpackedFloat → Bool

Returns true if the float is NaN.

Equations

• Float.Model.UnpackedFloat.notANumber.isNaN = true
• x✝.isNaN = false