A Coq Library on Floating-Point Arithmetic
This library was first designed by Laurent
Théry and Laurence
Rideau. Contributors now include Laurent Fousse, Guillaume
Melquiond and Sylvie Boldo (maintainer).
- All the versions of the library:
using Coq V7.4, V8.0, V8.1 or V8.2
are downloadable on
- Click here to access the library via various indexes (by module, definition, lemma...)
- The last developments are:
- To go back to the main page of
The following graph, made using dot,
describes the dependences between all the files of the library. All
the nodes are clickable to access directly the file.
The colors refer to the directory where the file lie and to the
subject matter: beige for the initial library, green for the
expansions, violet for the two's complement, blue for the elementary
functions evaluation and red for the other files.