The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

StackOverflow?

       - Benjamin

> On Nov 30, 2017, at 18:28, 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?