Exactly four little-endian budget bytes build base-256 iteration blocks.
Each block checks Stopped before entering; no unary budget conversion occurs.
680def iterateNormalizationNatural =
681 (lambda unrestricted digits : Bytes .
682 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
683 (lambda unrestricted seed : (family NormalizationNaturalState) .
684 (app
685 (bytes-eliminate
686 (lambda unrestricted remaining : Bytes .
687 (pi unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
688 (pi unrestricted seed : (family NormalizationNaturalState) .
689 (family NormalizationNaturalState))))
690 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
691 (lambda unrestricted seed : (family NormalizationNaturalState) . seed))
692 (lambda unrestricted head : Byte .
693 (lambda unrestricted tail : Bytes .
694 (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) . (pi unrestricted seed : (family NormalizationNaturalState) . (family NormalizationNaturalState))) .
695 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
696 (lambda unrestricted seed : (family NormalizationNaturalState) .
697 (continue
698 (lambda unrestricted state : (family NormalizationNaturalState) .
699 (repeatNormalizationNaturalSmall
700 (succ (byte-to-nat (byte 255)))
701 step
702 state))
703 (repeatNormalizationNaturalSmall (byte-to-nat head) step seed)))))))
704 digits)
705 step
706 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.