In formalizing real analysis we follow the development of Bishop [1]. Real numbers are represented by infinite sequences of rationals, which are required to converge at a certain rate. We have
and equality is given by
Some operations on reals are defined as follows:
We identify the rationals with the subset of the reals represented by constant sequences.
The definition of multiplication involves the canonical bound of a real number a, which is an integer Ka such that for all n, Ka > |a(n)|. We define Ka as the least integer greater than |a(1)| + 2.
The purpose of the case split is to ensure that the maximum of the canonical bounds of a and b is used.
We also define the following subsets of 
. Notice that a positive real
is a pair, consisting of a real and a positive integer. This integer is the
witness that the real is positive. Nonzero reals are defined similarly.
It is often convenient to think of positive reals as real numbers rather than as pairs, and in Bishop this simplification is made with the understanding that witnesses are always available when needed. Nuprl's display mechanism easily adopts this style of presentation by having a positive number and its first projection look the same. This goes for nonzero reals as well.
The following two operations are defined on 
and
.
And finally,
