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.
494def modelWord32FromDecimalDigitsTruncated =
495 (lambda unrestricted digits : Bytes .
496 (app
497 (bytes-eliminate
498 (lambda unrestricted current : Bytes .
499 (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)))
500 (lambda unrestricted accumulator : (family ModelWord32) . accumulator)
501 (lambda unrestricted head : Byte .
502 (lambda unrestricted tail : Bytes .
503 (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord32) . (family ModelWord32)) .
504 (lambda unrestricted accumulator : (family ModelWord32) .
505 (induction
506 (modelWord32Add (modelWord32TimesTen accumulator) (modelWord32DecimalDigit head)))))))
507 digits)
508 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.