coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there a type representing the reals set (R) ?

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Is there a type representing the reals set (R) ?
Date: Tue, 18 Nov 2014 08:24:42 -0800

On Tue, Nov 18, 2014 at 7:44 AM, CHAUVIN Barnabe
<barnabe.chauvin AT gmail.com>
wrote:
> This is not important, but I don't really understand .. in english there is
> no name for the reals set ? (To designate R in math)

Are you talking about the type of real numbers, or the subset which
contains all reals? The first is R, the second would just be Full_set
R.
--
Daniel Schepler

[Coq-Club] Is there a type representing the reals set (R) ?, CHAUVIN Barnabe, 11/17/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, John Wiegley, 11/17/2014
- Re: [Coq-Club] Is there a type representing the reals set (R) ?, Daniel Schepler, 11/17/2014
  - Re: [Coq-Club] Is there a type representing the reals set (R) ?, CHAUVIN Barnabe, 11/18/2014
    - Re: [Coq-Club] Is there a type representing the reals set (R) ?, Daniel Schepler, 11/18/2014