A computable real fraction is a function of type:

REALF = void -> (Int X REALF)

A computable real is a computable real fraction together with an exponent.

REAL = (REALF X Int)

The function "sum" computes the sum of two reals as follows: