The CReal
type implements (constructive) real numbers.
Note that the comparison operations on CReal
may diverge
since it is (by necessity) impossible to implementent them
correctly and always terminating.
This implementation is really David Lester's ERA package.