Legend:
Library
Module
Module type
Parameter
Class
Class type
Sorts implementing IEEE754 formats.
This module provides an infinite set of indexed sorts for floating point numbers defined in the IEEE754 standard.
This sorts are not referenced in the Core Theory (or any other theory in this library) and provided for user convenience. Any other format could be used with the Core Theory.
The names of parameter are taken from the IEEE 754-1985 standard section 3.6, table 3.5 on page 13. For the convenience, here is their meaning (refer the original standard for more detailed definitions):
k - storage width in bits;
p - precision in bits;
w - exponent field width in bits;
t - trailing significand field width in bits;
The module provides a set of common predefined formats as well as safe constructors to define uncommon formats.