  Real numbers do not admit an extensional procedure for observing discrete
information, such as the first digit of its decimal expansion, because every
extensional, computable map from the reals to the integers is constant, as is
well known. We overcome this by considering real numbers equipped with
additional structure, which we call a locator. With this structure, it is
possible, for instance, to construct a signed-digit representation or a Cauchy
sequence, and conversely these intensional representations give rise to a
locator. Although the constructions are reminiscent of computable analysis,
instead of working with a notion of computability, we simply work
constructively to extract observable information, and instead of working with
representations, we consider a certain locatedness structure on real numbers.

Logic;Logic in Computer Science