The Coq mailing list

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

I am currently exploring the standard library, and I feel like the 
different theories (Like for example Reals, Sets, Logic ...) are not 
really working together ..

I was actually looking for a type of the reals set (Exactly like the 
inductive type Integers), to be able to use the Sets theories 
(Ensembles.v ... and especially the order theorems/lemmas).
In Rdefinitions, I found the is_upper_bound definition, which represent 
the R set with the type R->Prop. It would be more understandable if it 
would be "Ensemble R", isn't it ? (This is the reason why I said I feel 
like the theories are not working together ..)

Nevertheless, I didn't find such a defintion (the R set). Is-it my 
mistake, or it is impossible to define such a type, because of the 
definition of the reals in coq (with axioms) ?
Or maybe I am free to use almost the same definition as Integers, i.e. 
"Inductive Reals : Ensemble R := Reals_defn : forall x:nat, In R Reals 
x." and then define a partial order on this set ("PO R") ?

Kind regards,
Barnabé Chauvin