2.7.38 Types Tutorial Exercise 6

The full rule for leap years is that they occur in every year divisible by four, except that they don’t occur in years divisible by 100, except that they do in years divisible by 400. We could work out the answer by carefully counting the years divisible by four and the exceptions, but there is a much simpler way that works even if we don’t know the leap year rule.

Let’s assume the present year is 1991. Years have 365 days, except that leap years (whenever they occur) have 366 days. So let’s count the number of days between now and then, and compare that to the number of years times 365. The number of extra days we find must be equal to the number of leap years there were.

1:  <Mon Jan 1, 10001>     2:  <Mon Jan 1, 10001>     1:  2925593
    .                      1:  <Tue Jan 1, 1991>          .
                               .

  ' <jan 1 10001> RET         ' <jan 1 1991> RET          -

3:  2925593       2:  2925593     2:  2925593     1:  1943
2:  10001         1:  8010        1:  2923650         .
1:  1991              .               .
    .

  10001 RET 1991      -               365 *           -

There will be 1943 leap years before the year 10001. (Assuming, of course, that the algorithm for computing leap years remains unchanged for that long. See Date Forms, for some interesting background information in that regard.)