The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

On Sun, Jun 24, 2012 at 12:21 AM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> I was actually thinking about a type-theoretical model of real numbers 
> which would use both a number of meaningful digits *and* the exponent. 
> Neither of the standard models seems to use exponent as a part of the 
> description.

That is exactly what most implementations of real number do. For
example Robbert Krebbers and Bas Spitter's, the first link I provided,
works with dyadic rationals (which are rationals of the form m * 2^e,
just like you'd like them to be). Their implementation is written in
Coq.

With kind regards,

Andrej