|
|
|
|
|
|
by singularity2001
15 hours ago
|
|
|
there is a practical reason to get rid of the fantasy reals and restrict oneself to normal reals or some other new invention: Since Lean has become more popular as a proving system I've stumbled upon one very annoying feature of reals: they are not computably comparable. The system says you can never know whether two arbitrary real numbers are the same because you don't have enough time to compare them. |
|
|