Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

def · lines 7559–7582

iterateCoreNaturalWork

Full file
7559def iterateCoreNaturalWork =
7560  (lambda unrestricted digits : Bytes .
7561    (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) .
7562      (lambda unrestricted seed : (family CoreNaturalWorkState) .
7563        (app
7564          (bytes-eliminate
7565            (lambda unrestricted remaining : Bytes .
7566              (pi unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) .
7567                (pi unrestricted seed : (family CoreNaturalWorkState) .
7568                  (family CoreNaturalWorkState))))
7569            (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) .
7570              (lambda unrestricted seed : (family CoreNaturalWorkState) . seed))
7571            (lambda unrestricted head : Byte .
7572              (lambda unrestricted tail : Bytes .
7573                (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) . (pi unrestricted seed : (family CoreNaturalWorkState) . (family CoreNaturalWorkState))) .
7574                  (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) .
7575                    (lambda unrestricted seed : (family CoreNaturalWorkState) .
7576                      (continue
7577                        (lambda unrestricted state : (family CoreNaturalWorkState) .
7578                          (repeatCoreNaturalWorkSmall (byte-to-nat (byte 10)) step state))
7579                        (repeatCoreNaturalWorkSmall (byte-to-nat head) step seed)))))))
7580            digits)
7581          step
7582          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.