The Coq mailing list

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

Hello club !

Playing with the CoRN library, I have a few questions about how Reals 
work :
 - I understood the structures from CSetoid to CReals, but I don't 
really understand the difference between IR and CR ? I know CR stand for 
Computational reals, but what does IR means ?
 - What is exactly the aim of the RasIR and IRasR definitions ? Do they 
allow computation of coq reals (for example 4%R + 3%R ? )
 - When to use CR or IR or R in a proof ? (And why rather this one). Of 
course, I guess it depends on the circumstances ..
 - Let's assume I have a subgoal  2<3  (the type of the number depends 
on my previous question, but they are reals numbers), what is the best 
way to solve it ? Use CoRN computation (I'm talking of a simple 
inequality or equality) ?

Thanks for your attention !
These questions might seem weird or even destructured, but I'm a 
complete beginner ..

Best regards.