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.)

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.

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.

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.