coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] real numbers

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] real numbers
Date: Sat, 23 Jun 2012 04:57:45 -0400

I wonder if someone tried to build a constructive model of real numbers
starting with the floating point representations of increasing precision?

Vladimir.

[Coq-Club] real numbers, Vladimir Voevodsky, 06/23/2012
- Re: [Coq-Club] real numbers, Jonas Oberhauser, 06/23/2012
  - Re: [Coq-Club] real numbers, Daniel Schepler, 06/25/2012
    - Re: [Coq-Club] real numbers, Guillaume Melquiond, 06/25/2012
      - Re: [Coq-Club] real numbers, Yves Bertot, 06/26/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
  - Re: [Coq-Club] real numbers, Freek Wiedijk, 06/23/2012
    - Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
      - Re: [Coq-Club] real numbers, Freek Wiedijk, 06/23/2012
        
        Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
  - Re: [Coq-Club] real numbers, Vladimir Voevodsky, 06/24/2012