This module defines an arbitrary precision floating point type and
its operations. It should be viewed more abstractly as an instance
ERRealBase when used as interval endpoints.
- data ERFloat
A floating point number with a given but arbitrary precision represented by its
- base: 2.
- granularity specifies the bit-size of both the significand and the exponent
- special values: NaN, signed Infinity and signed Zero
- no denormalised numbers
- operations unify the granularity of their operands to the maximum
- Rounding is always towards +Infinity. For field operations, the rounded result is as close as possible to the exact result.