Decimal digit bytes, most significant first, to a word modulo 2^32; one
step per digit. Callers check the bytes are digits and the value fits.
478def modelWord32FromDecimalDigitsTruncated =
479 (lambda unrestricted digits : Bytes .
480 (app
481 (bytes-eliminate
482 (lambda unrestricted current : Bytes .
483 (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)))
484 (lambda unrestricted accumulator : (family ModelWord32) . accumulator)
485 (lambda unrestricted head : Byte .
486 (lambda unrestricted tail : Bytes .
487 (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)) .
488 (lambda unrestricted accumulator : (family ModelWord32) .
489 (induction
490 (modelWord32Add (modelWord32TimesTen accumulator) (modelWord32DecimalDigit head)))))))
491 digits)
492 modelWord32Zero))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.