IEEE rounding modes for Model

This type provides nearest-even rounding and the three directed rounding attributes. The broader quantization-policy vocabulary also contains nearest-away and stochastic rounding.

This is the shared mode definition for executable rounding and its proofs.

inductive FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode : Type

Deterministic IEEE-754 rounding-direction attribute.

• nearestEven : IEEERoundingMode

  Round to the nearest representable value, breaking ties toward an even significand.

• towardZero : IEEERoundingMode

  Round toward zero.

• towardPositiveInfinity : IEEERoundingMode

  Round toward positive infinity.

• towardNegativeInfinity : IEEERoundingMode

  Round toward negative infinity.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqIEEERoundingMode : DecidableEq IEEERoundingMode

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIEEERoundingMode.repr : IEEERoundingMode → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIEEERoundingMode : Repr IEEERoundingMode

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.all : List IEEERoundingMode

All constructors of IEEERoundingMode, in their shared traversal order.

Update this list when adding a constructor; callers can use it without duplicating the enumeration.

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.name : IEEERoundingMode → String

A concise, stable name for diagnostics and interchange files.

The directed modes use the customary towardPositive and towardNegative spellings; their constructors retain the more explicit Infinity suffix used in proofs and APIs.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.instToString : ToString IEEERoundingMode

def FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.toRoundingMode : IEEERoundingMode → Numerics.RoundingMode

The quantization-policy rounding mode with the same direction.

Numerics.RoundingMode also contains nearest-away and stochastic rounding, which have no constructor in IEEERoundingMode; this map is therefore an embedding, not a bijection.

The optional FloatLib.IEEERounding scope provides mathematical spellings for the two directed infinity modes. Keeping these notations scoped prevents them from changing the meaning of ∞ in files that use extended real numbers.

def FloatLib.IEEERounding.«term+∞» : Lean.ParserDescr

Round toward positive infinity. Requires open scoped FloatLib.IEEERounding.

def FloatLib.IEEERounding.«term-∞» : Lean.ParserDescr

Round toward negative infinity. Requires open scoped FloatLib.IEEERounding.