Types Tutorial Exercise 1

If the number is the square root of @c{$\pi$} pi times a rational number, then its square, divided by @c{$\pi$} pi, should be a rational number.

1:  1.26508260337    1:  0.509433962268   1:  2486645810:4881193627
    .                    .                    .

                         2 ^ P /              c F

Technically speaking this is a rational number, but not one that is likely to have arisen in the original problem. More likely, it just happens to be the fraction which most closely represents some irrational number to within 12 digits.

But perhaps our result was not quite exact. Let's reduce the precision slightly and try again:

1:  0.509433962268     1:  27:53
    .                      .

    U p 10 RET             c F

Aha! It's unlikely that an irrational number would equal a fraction this simple to within ten digits, so our original number was probably sqrt(27 pi / 53).

Notice that we didn't need to re-round the number when we reduced the precision. Remember, arithmetic operations always round their inputs to the current precision before they begin.