Add Floats to standard library

All supported floating point operations are defined on specification floats.
Then we register the primitive type and functions, and add conversion
functions to and from the specification type.
Finally we put axioms to state that primitive operations behave exactly
the same as specification operations.

CREDITS: Most of the code inside SpecFloat is adapted from the Flocq
library.

NOTE: For the moment this code will not compile if native compilation is
enabled in the configuration phase. This will be resolved later when
native_compute will be supported by primitive floats.

So please use option "-native-compiler no" in ./configure currently.

0 files changed, 0 insertions, 0 deletions