data.real The real numbers: classically, as a quotient type; constructively, as a setoid. basic : the reals as a commutative ring (constructive) order : the reals as an ordered ring (constructive) division : the reals as a discrete linear ordered field (classical) complete : the reals are Cauchy complete (classical)