CR is one of the 3 types defining constructive reals in CoRN. It by applying a completion monad over the metric space of rational numbers. This completion monad is defined in Section 3.2 of:
Krebbers, R., and Spitters, B. (2013). Type classes for efficient exact real arithmetic in Coq. LMCS 9.
It's Coq definition can be found at here