569def magnitudeIterate =
570 (lambda erased State : Type 0 .
571 (lambda unrestricted digits : Bytes .
572 (lambda unrestricted step : (pi unrestricted value : State . State) .
573 (lambda unrestricted seed : State .
574 (app
575 (bytes-eliminate
576 (lambda unrestricted rest : Bytes .
577 (pi unrestricted step : (pi unrestricted value : State . State) .
578 (pi unrestricted seed : State . State)))
579 (lambda unrestricted step : (pi unrestricted value : State . State) .
580 (lambda unrestricted seed : State . seed))
581 (lambda unrestricted head : Byte .
582 (lambda unrestricted tail : Bytes .
583 (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted value : State . State) . (pi unrestricted seed : State . State)) .
584 (lambda unrestricted step : (pi unrestricted value : State . State) .
585 (lambda unrestricted seed : State .
586 (continue
587 (lambda unrestricted state : State .
588 (magnitudeRepeatSmall State (byte-to-nat (byte 10)) step state))
589 (magnitudeRepeatSmall State (byte-to-nat head) step seed)))))))
590 digits)
591 step
592 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.