P3109 comparisons and extrema

Comparisons are unordered at NaN. The ten extrema differ in NaN handling, magnitude ordering, and preference for finite operands. Equal magnitudes use numerical order to resolve the sign: minimum selects the negative operand, maximum the positive operand.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §§4.11–4.12.

def FloatLib.Floats.Formats.P3109.Arithmetic.less : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Bool

Strict extended-real comparison; NaN is unordered, including with itself.

def FloatLib.Floats.Formats.P3109.Arithmetic.equal : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Bool

Numerical equality, ignoring NaN payloads by making every NaN comparison false.

def FloatLib.Floats.Formats.P3109.Arithmetic.lessEqual (left right : Numerics.NumericalValue ℚ) : Bool

Non-strict extended-real comparison; NaN remains unordered.

def FloatLib.Floats.Formats.P3109.Arithmetic.greater (left right : Numerics.NumericalValue ℚ) : Bool

Reverse strict comparison.

def FloatLib.Floats.Formats.P3109.Arithmetic.greaterEqual (left right : Numerics.NumericalValue ℚ) : Bool

Reverse non-strict comparison.

def FloatLib.Floats.Formats.P3109.Arithmetic.minimum : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Minimum, propagating either NaN operand.

def FloatLib.Floats.Formats.P3109.Arithmetic.maximum : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Maximum, propagating either NaN operand.

def FloatLib.Floats.Formats.P3109.Arithmetic.numberVariant (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Ignore a single NaN before applying an extremum; two NaNs yield the canonical NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.minimumNumber : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Minimum with a numerical operand preferred to NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.maximumNumber : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Maximum with a numerical operand preferred to NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.minimumMagnitude : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Minimum absolute value, resolving equal magnitudes toward the numerically smaller datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.maximumMagnitude : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Maximum absolute value, resolving equal magnitudes toward the numerically larger datum.

def FloatLib.Floats.Formats.P3109.Arithmetic.minimumMagnitudeNumber : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Minimum magnitude with a numerical operand preferred to NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.maximumMagnitudeNumber : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Maximum magnitude with a numerical operand preferred to NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.finiteVariant (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Prefer the finite operand to an infinity, then use the supplied number extremum.

def FloatLib.Floats.Formats.P3109.Arithmetic.minimumFinite : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Minimum finite variant: finite values outrank infinities, which outrank NaN.

def FloatLib.Floats.Formats.P3109.Arithmetic.maximumFinite : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Maximum finite variant: finite values outrank infinities, which outrank NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.less {format : Formats.P3109.Format} (left right : P3109 format) : Bool

Strict comparison of decoded operands, with NaN unordered.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.lessEqual {format : Formats.P3109.Format} (left right : P3109 format) : Bool

Non-strict comparison of decoded operands, with NaN unordered.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.equal {format : Formats.P3109.Format} (left right : P3109 format) : Bool

Numerical equality; NaN compares unequal to every operand.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.greater {format : Formats.P3109.Format} (left right : P3109 format) : Bool

Strict reverse comparison of decoded operands.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.greaterEqual {format : Formats.P3109.Format} (left right : P3109 format) : Bool

Non-strict reverse comparison of decoded operands.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimum {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Minimum with NaN propagation and the supplied final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximum {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Maximum with NaN propagation and the supplied final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumNumber {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Minimum with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumNumber {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Maximum with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumMagnitude {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Minimum magnitude, with negative sign preferred at a tie.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumMagnitude {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Maximum magnitude, with positive sign preferred at a tie.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumMagnitudeNumber {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Minimum magnitude with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumMagnitudeNumber {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Maximum magnitude with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumFinite {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Minimum preferring finite values to infinity and infinity to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumFinite {format : Formats.P3109.Format} (left right : P3109 format) (policy : Formats.P3109.ProjectionPolicy := Formats.P3109.ProjectionPolicy.nearestEven) : P3109 format

Maximum preferring finite values to infinity and infinity to NaN.