Internal arithmetic on canonical decimal digit bytes, least significant first.
Zero is empty; every digit is 0..9 and the final digit is nonzero.
The checked owner validates external input before calling these operations.
Whole-value Nat conversion is only for existing unary values or bounded carries.
Normalization and addition assemble a BytesBuilder and materialize once;
repeated bytes-cons of complete suffixes would copy quadratic byte volume.
A carry digit uses explicit low-byte conversion of total + 246 for total
in 10..19, which equals total - 10. Addition preserves canonical inputs.
13def magnitudeNormalize =
14 (lambda unrestricted digits : Bytes .
15 (bytes-builder-build
16 (second
17 (bytes-eliminate
18 (lambda unrestricted rest : Bytes . (sigma unrestricted active : Nat . BytesBuilder))
19 (pair (sigma unrestricted active : Nat . BytesBuilder) zero (bytes-builder-empty))
20 (lambda unrestricted head : Byte .
21 (lambda unrestricted tail : Bytes .
22 (lambda unrestricted continue : (sigma unrestricted active : Nat . BytesBuilder) .
23 (app
24 (nat-eliminate
25 (lambda unrestricted flag : Nat .
26 (pi unrestricted force : Nat .
27 (sigma unrestricted active : Nat . BytesBuilder)))
28 (lambda unrestricted force : Nat .
29 (pair
30 (sigma unrestricted active : Nat . BytesBuilder)
31 (succ zero)
32 (bytes-builder-append
33 (bytes-builder-chunk (bytes-cons head b""))
34 (second continue))))
35 (lambda unrestricted predecessor : Nat .
36 (lambda unrestricted induction : (pi unrestricted force : Nat . (sigma unrestricted active : Nat . BytesBuilder)) .
37 (lambda unrestricted force : Nat . continue)))
38 (Std.Natural/naturalAnd
39 (byte-equal head (byte 0))
40 (Std.Natural/naturalIsZero (first continue))))
41 zero))))
42 digits))))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.