Floating-Point Configuration

This module defines FloatCfg, the precision and exponent-range parameters that describe a floating-point format, along with the available RoundingModes and a Rounding typeclass selecting the mode in scope.

structure FloatCfg : Type

A floating-point format: a precision prec and an exponent range [emin, emax].

• prec : ℕ

  The precision: the number of representable mantissa steps.

• emin : ℤ

  The minimum exponent of the format.

• emax : ℤ

  The maximum exponent of the format.

• emin_lt_emax : self.emin < self.emax

  The exponent range is nonempty.

• prec_pos : 0 < self.prec

  The precision is positive.

inductive RoundingMode : Type

The supported rounding modes for converting a rational to a float.

• nearest : RoundingMode

  Round to the nearest representable value (ties to even).

• down : RoundingMode

  Round toward negative infinity.

• up : RoundingMode

  Round toward positive infinity.

• tozero : RoundingMode

  Round toward zero.

• toinf : RoundingMode

  Round away from zero (toward infinity in magnitude).

class Rounding : Type

A typeclass selecting the RoundingMode in scope.

• mode : RoundingMode

  The rounding mode used by the operations in scope.