P3109 comparisons and extrema

Comparisons are unordered at NaN. compare is the order behind == on P3109 values, so NaN compares unequal to itself. The ten extrema differ in NaN handling, magnitude ordering, and preference for finite operands. Equal magnitudes use numerical order to resolve the sign, so minimum selects the negative operand and maximum the positive one.

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, with NaN unordered even against 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, with NaN 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 give 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.

def FloatLib.Floats.Formats.P3109.Arithmetic.clamp (value lower upper : Numerics.NumericalValue ℚ) : Numerics.NumericalValue ℚ

Report §4.11.4 clamp, propagating NaN and rejecting reversed bounds.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.clamp {format : Formats.P3109.Format} (value lower upper : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Clamp value to [lower, upper] with exact bound checks, then project once into target, by default the format of value. Reversed bounds and NaN yield 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, under which NaN is 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.compare {format : Formats.P3109.Format} (left right : P3109 format) : Option Ordering

Order of two decoded operands, or none when either is NaN.

Infinities are ordered at the ends of the extended reals and equal when their signs agree.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimum {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Minimum with NaN propagation and the supplied final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximum {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Maximum with NaN propagation and the supplied final projection.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumNumber {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Minimum with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumNumber {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Maximum with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumMagnitude {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Minimum magnitude, with negative sign preferred at a tie.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumMagnitude {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Maximum magnitude, with positive sign preferred at a tie.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumMagnitudeNumber {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Minimum magnitude with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.maximumMagnitudeNumber {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Maximum magnitude with a numerical operand preferred to NaN.

@[inline]

def FloatLib.Floats.ExecFloat.P3109.minimumFinite {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

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) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) : P3109 target

Maximum preferring finite values to infinity and infinity to NaN.