Specification of floating-point arithmetic
This specification is mostly borrowed from the
IEEE754.Binary module
of the Flocq library (see
http://flocq.gforge.inria.fr/)
Inductive specification of floating-point numbers
Similar to
Flocq.IEEE754.Binary.full_float, but with no NaN payload.
Parameterized definitions
prec is the number of bits of the mantissa including the implicit one;
emax is the exponent of the infinities.
For instance, Binary64 is defined by
prec = 53 and
emax = 1024.