Exactly four little-endian budget bytes build base-256 iteration blocks.
Each block checks Stopped before entering; no unary budget conversion occurs.
497def iterateNormalizationPayload =
498 (lambda unrestricted digits : Bytes .
499 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
500 (lambda unrestricted seed : (family NormalizationPayloadState) .
501 (app
502 (bytes-eliminate
503 (lambda unrestricted remaining : Bytes .
504 (pi unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
505 (pi unrestricted seed : (family NormalizationPayloadState) .
506 (family NormalizationPayloadState))))
507 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
508 (lambda unrestricted seed : (family NormalizationPayloadState) . seed))
509 (lambda unrestricted head : Byte .
510 (lambda unrestricted tail : Bytes .
511 (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) . (pi unrestricted seed : (family NormalizationPayloadState) . (family NormalizationPayloadState))) .
512 (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
513 (lambda unrestricted seed : (family NormalizationPayloadState) .
514 (continue
515 (lambda unrestricted state : (family NormalizationPayloadState) .
516 (repeatNormalizationPayloadSmall
517 (succ (byte-to-nat (byte 255)))
518 step
519 state))
520 (repeatNormalizationPayloadSmall (byte-to-nat head) step seed)))))))
521 digits)
522 step
523 seed))))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.