def Float.Model.UnpackedFloat.compare : UnpackedFloat → UnpackedFloat → Option Ordering

Computes the ordering between the two floats as specificed by IEEE. Returns an Option Ordering to account for the fact that NaN is incomparable with everything. Also, positive and negative zero are equal.

Important: this operation only works correctly if the two inputs are in canonical form for a common format (see the docstring for UnpackedFloat for details.)

Equations

• One or more equations did not get rendered due to their size.
• Float.Model.UnpackedFloat.notANumber.compare x✝ = none
• x✝.compare Float.Model.UnpackedFloat.notANumber = none
• (Float.Model.UnpackedFloat.infinity s₁).compare (Float.Model.UnpackedFloat.infinity s₂) = some (compare s₁ s₂)
• (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive).compare x✝ = some Ordering.gt
• (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative).compare x✝ = some Ordering.lt
• x✝.compare (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.positive) = some Ordering.lt
• x✝.compare (Float.Model.UnpackedFloat.infinity Float.Model.UnpackedFloat.Sign.negative) = some Ordering.gt
• (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos).compare (Float.Model.UnpackedFloat.zero sign) = some Ordering.gt
• (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos).compare (Float.Model.UnpackedFloat.zero sign) = some Ordering.lt
• (Float.Model.UnpackedFloat.zero sign).compare (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.positive mantissa exponent mantissa_pos) = some Ordering.lt
• (Float.Model.UnpackedFloat.zero sign).compare (Float.Model.UnpackedFloat.finite Float.Model.UnpackedFloat.Sign.negative mantissa exponent mantissa_pos) = some Ordering.gt
• (Float.Model.UnpackedFloat.zero sign).compare (Float.Model.UnpackedFloat.zero sign_1) = some Ordering.eq

def Float.Model.UnpackedFloat.le (a b : UnpackedFloat) : Bool

Determines whether a is less than or equal to b according to IEEE rules.

This is not a total ordering, and ≤ is not reflexive.

Equations

• a.le b = Option.any (fun (x : Ordering) => x.isLE) (a.compare b)

def Float.Model.UnpackedFloat.lt (a b : UnpackedFloat) : Bool

Determines whether a is less than b according to IEEE rules.

This is not a total ordering.

Equations

• a.lt b = (a.compare b == some Ordering.lt)

def Float.Model.UnpackedFloat.beq (a b : UnpackedFloat) : Bool

Determines whether a is equal to b according to IEEE rules.

This is not a reflexive relation.

Equations

• a.beq b = (a.compare b == some Ordering.eq)