Editing Constructive analysis (section)

====Moduli====
As the [[Maximum and minimum|maximum]] on a finite set of rationals is decidable, an absolute value map on the reals may be defined and [[Cauchy sequence|Cauchy convergence]] and limits of sequences of reals can be defined as usual.

A [[modulus of convergence]] is often employed in the constructive study of Cauchy sequences of reals, meaning the association of any <math>\varepsilon > 0</math> to an appropriate index (beyond which the sequences are closer than <math>\varepsilon</math>) is required in the form of an explicit, strictly increasing function <math>\varepsilon\mapsto N(\varepsilon)</math>. Such a modulus may be considered for a sequence of reals, but it may also be considered for all the reals themselves, in which case one is really dealing with a sequence of pairs.