The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

On 16/08/2017 15:33, Guillaume Melquiond wrote:
> 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
>

To all: if this is a question which tends to come up regularly is there 
some way we could make the answer easier to find?

Gaëtan Gilbert

On 01/12/2017 00:23, Kevin Sullivan wrote:
> What library or libraries should I consider as I need to represent 
> concrete floating point numbers, do calculations with them, and prove 
> properties about them using the current version of Coq?