506def magnitudeMultiplyDigit =
507 (lambda unrestricted digits : Bytes .
508 (lambda unrestricted factor : Byte .
509 (magnitudeNormalize
510 (app
511 (bytes-eliminate
512 (lambda unrestricted rest : Bytes . (pi unrestricted carry : Nat . Bytes))
513 (lambda unrestricted carry : Nat . (magnitudeFromNatural carry))
514 (lambda unrestricted head : Byte .
515 (lambda unrestricted tail : Bytes .
516 (lambda unrestricted continue : (pi unrestricted carry : Nat . Bytes) .
517 (lambda unrestricted carry : Nat .
518 (app
519 (lambda unrestricted total : Nat .
520 (app
521 (lambda unrestricted nextCarry : Nat .
522 (bytes-cons
523 (nat-to-byte
524 (Std.Natural/naturalSaturatingSubtract
525 total
526 (Std.Natural/naturalMultiply nextCarry (byte-to-nat (byte 10)))))
527 (continue nextCarry)))
528 (Std.Natural/naturalDivideUnchecked total (byte-to-nat (byte 10)))))
529 (Std.Natural/naturalAdd
530 (Std.Natural/naturalMultiply (byte-to-nat head) (byte-to-nat factor))
531 carry))))))
532 digits)
533 zero))))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.