The problem is that Cauchy sequences are too powerful. The intuitionist/constructive version of "rationally approximable" requires a procedure to approximate a

The problem is that Cauchy sequences are too powerful. The intuitionist/constructive version of "rationally approximable" requires a procedure to approximate a number to any requested degree of precision, but cannot guarantee that equality is decideable. My use of discrete was informal and in response to the thread here which equated discarding the notion on the continuum with saying the universe is "discrete". More precise in the topology sense is that the rationals are not compact