Does a run of decimal digits denote a magnitude at most 2^63 - 1? Decided
on the DIGITS, never on the natural: fewer than nineteen digits always fit,
more never do, and nineteen fit when they are not lexicographically above
9223372036854775807. A runtime natural costs ~164 bytes per unit of
magnitude and the checker's division is unary, so neither 2^63 nor a
63-step halving of a 2^63-scale value is computable on either side; the
string comparison costs nineteen byte comparisons at most.
The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.