The Coq mailing list

[CHAUVIN Barnabe <barnabe.chauvin AT gmail.com>]

On 17/11/2014 23:45, Daniel Schepler wrote:
> You could also certainly define a partial order on R using Rle - 
though I'm not sure why you're combining that in the same sentence with 
the other question.
I actually need a partial order such as the Integers' one (the nat_po), 
in order to work with real subsets bounds etc ..
That's why I asked before if there was a definition of the reals set.

Eventually, I'm just going to define such a type, in the same way the 
type Integers is defined.


> And then, I'm not sure "Reals" is a very descriptive name for it.

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)

-- Barnabé Chauvin