thor
Reputation: 22530
What's the difference between `Reals` and `Coq.Reals.*` in Coq?
In proving general facts like inequalities and polynomial equations, what's the difference between importing Reals and things like Coq.Reals.{Rineq, R_sqrt, ...}?
I started from searching specific facts/theorems and ended up in using the latter, but I've seen others using just Reals. Is it easier or more comprehensive to just use Reals?
Suspecting it's a legacy thing, I tried to import just Coq.Reals but it does not seem to exist (Coq 8.5 beta 3).
Upvotes: 0
Views: 180
Answers (0)
Related Questions
- What is the meaning of "|-" in coq, and how do I find the definitions for the other seemingly undocumented notations?
- Overloading operators in Coq via typeclasses and notation scopes: Is there anything special about the '+' and '*' symbols?
- Real numbers in Coq
- Stronger completeness axiom for real numbers in Coq
- Coq Reals and Ssreflect GRings
- Notations in Coq
- how to figure out what "=" means in different types in coq
- Coq Real numbers -lexing and parsing 3.14
- How to use Coq GenericMinMax to prove facts about the reals
- How to automatically prove simple equality of real numbers in Coq?