Compiler.NaturalMagnitudeArithmetic

49def magnitudeSuccessorDigits =
50  (lambda unrestricted digits : Bytes .
51    (app
52      (bytes-eliminate
53        (lambda unrestricted rest : Bytes . (pi unrestricted force : Nat . Bytes))
54        (lambda unrestricted force : Nat . (bytes 1))
55        (lambda unrestricted head : Byte .
56          (lambda unrestricted tail : Bytes .
57            (lambda unrestricted continue : (pi unrestricted force : Nat . Bytes) .
58              (lambda unrestricted force : Nat .
59                (app
60                  (nat-eliminate
61                    (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
62                    (lambda unrestricted force : Nat .
63                      (bytes-cons (nat-to-byte (succ (byte-to-nat head))) tail))
64                    (lambda unrestricted predecessor : Nat .
65                      (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
66                        (lambda unrestricted force : Nat . (bytes-cons (byte 0) (continue zero)))))
67                    (byte-equal head (byte 9)))
68                  zero)))))
69        digits)
70      zero))