The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

> 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?

Search "float":
https://github.com/coq/coq/wiki

On Fri, Dec 1, 2017 at 12:28 AM, 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?