Source radices are fixed by the grammar. Checked addition chains avoid
a general 64-step multiply per digit, while Std.Word remains the arithmetic
owner. Every intermediate fits whenever the final nonnegative product fits;
an intermediate overflow therefore proves the literal cannot fit U64.
437def integerLiteralCheckedAdd =
438 (lambda unrestricted left : (family ModelWord64) .
439 (lambda unrestricted right : (family ModelWord64) .
440 (eliminate
441 ModelWord64CheckedResult
442 (lambda unrestricted current : (family ModelWord64CheckedResult) .
443 (family IntegerLiteralU64StepResult))
444 (stdU64AddChecked left right)
445 (branch
446 ModelWord64CheckedSucceeded
447 value
448 .
449 (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepSucceeded value))
450 (branch
451 ModelWord64CheckedFailed
452 error
453 .
454 (constructor IntegerLiteralU64StepResult IntegerLiteralU64StepFailed)))))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.