AlphaGitHub
Source/Packages

Model.Word32

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

508 lines41 declarations18.3 KiBSHA-256 7f230128ec8c
Download exact fileView at revision426597bda5753d86c4

def · lines 239–256

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).
239def modelWord32FromNaturalDivided =
240  (lambda unrestricted value : Nat .
241    (app
242      (lambda unrestricted quotient1 : Nat .
243        (app
244          (lambda unrestricted quotient2 : Nat .
245            (app
246              (lambda unrestricted quotient3 : Nat .
247                (constructor
248                  ModelWord32
249                  ModelWord32Value
250                  (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
251                  (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
252                  (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
253                  (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
254              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
255          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
256      (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.