The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Thank you. Flocq was an obvious candidate. Interval less so. I will look at the latter to, so thanks, again for that. -Kevin

On Thu, Nov 30, 2017 at 6:28 PM, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

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?