The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 15/08/2017 08:05, karsar wrote:
> What would be a natural choice of float number library if you want to do
> some
> computations with floats inside Coq (like it's done for integers and nats, 
> I know it could be slow) , as well as reason about their properties? 
> It would be nice to provide a minimal example script showing how you
> import the library
> and example of the addition of two floats as a demonstration.

Both the Flocq and Interval libraries contain computationally effective
floating-point components. Which one to use and how to use it depend on
your use case. Do you need the floating-point numbers to be compliant
with the IEEE-754 standard? What kind of reasoning do you want to
perform on them? How efficient do you want the computations to be?

Best regards,

Guillaume