AlphaGitHub
Source/Packages

Model.Word32

packages/foundation/standard/src/Model/Word32.alpha

492 lines41 declarations17.0 KiBSHA-256 eb985612415b
Download exact fileView at revisionf5034773ad4bb52133

def · lines 364–381

modelWord32FromNaturalDivided

Full file
General path: four divisions by 256 (a fold over the value each). Reached only for values of 256 and above; `modelWord32FromNaturalTruncated` takes the O(1) byte path below that (D17).
364def modelWord32FromNaturalDivided =
365  (lambda unrestricted value : Nat .
366    (app
367      (lambda unrestricted quotient1 : Nat .
368        (app
369          (lambda unrestricted quotient2 : Nat .
370            (app
371              (lambda unrestricted quotient3 : Nat .
372                (constructor
373                  ModelWord32
374                  ModelWord32Value
375                  (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
376                  (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
377                  (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
378                  (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
379              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
380          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
381      (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))

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.