IR is one of the 3 types defining constructive reals in CoRN. It is defined as computable cauchy sequences of rationals.
It's formal definition can be found at here
For more, see Bishop, E., and Bridges, D. (1985). Constructive Analysis (Springer Science & Business Media).