The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

On Sun, Jun 24, 2012 at 9:06 AM, Freek Wiedijk 
<freek AT cs.ru.nl>
 wrote:
> the choice of dyadic rationals for the Cauchy sequences

This was already an explicit wish in our work:
Russell O'Connor and Bas Spitters
A computer verified, monadic, functional implementation of the integral.
http://dx.doi.org/10.1016/j.tcs.2010.05.031

But is was only done here:
Robbert Krebbers and Bas Spitters Computer certified efficient exact
reals in Coq
http://arxiv.org/abs/1105.2751 CICM'11 LNCS 90-106, 2011.

Regarding the change to type classes.
We try to have the general work available here
http://math-classes.org/

Not all of corn has been ported to type classes and it is unlikely the we 
will.
It is not so clear what would be the advantage of this. Some parts of
the library are not used anymore.


I would also like to mention the work by Cyril Cohen:
Reasoning about big enough numbers in Coq
http://perso.crans.org/cohen/papers/proposal_coq2012.pdf

It contains some nice tactics for reasoning about real numbers.

Best,

Bas