The definition of reals given in this programming language amounts to Real := Nat -> Rat, with the interpretation being that the real number is represented as t

The definition of reals given in this programming language amounts to Real := Nat -> Rat, with the interpretation being that the real number is represented as the limit of this function as the argument increases to infinity. Snazzy, but not quite right. (A footnote hints that it may not be quite right.) First, the encoding permits you to write down functions that diverge to infinity. So the type, Real, includes objects which are not reals. You may say, well, those objects are various encodings of infinity, and this type represents the reals together with infinity. Ok, but now consider what happens with these diverging functions when you operate on them. They do not all encode the same infinity. A function f(n) = n^2 diverges way faster than g(n) = n, so that f - g is decidedly still diverging, though f - f would encode zero. But it's worse: The limit isn't supposed to change if you shift the input by a finite amount. That should give equivalent encodings, right? But f(n+1) - f(n) does not encode 0, but rather some infinity. Even g(n+1) - g(n) encodes 1. The moral is that the limit-taking operation does not commute with the arithmetic operations, so you can't safely define arithmetic over this encoding of the reals in the presence of diverging functions. Second, it gets worse still: You can have functions with multiple limits. For example, h(n) = (-1)^(n%2), which alternates between plus and minus 1. Such functions in a certain way encode multiple reals at the same time! In summary, this data type does not work as a real type. It must be constrained so that the limit in question always exists and is unambiguous. I'd suggest pairing the type up with an integer (or rational) to serve as an upper bound, and interpreting the function to encode the real which is the lesser of the bound and the limsup (not the limit) of the function.