AlphaGitHub
Source/Packages

Realization.Nvidia.SM86.AdamWSM86

packages/realizations/cooperative/nvidia-sm86/src/Realization/Nvidia/SM86/AdamWSM86.alpha

1,127 lines173 declarations39.3 KiBSHA-256 0c5cdf90be84
Download exact fileView at revision426597bda5753d86c4

def · lines 261–276

adamWF32Unsigned32FromNatural

Full file
261def adamWF32Unsigned32FromNatural =
262  (lambda unrestricted value : Nat .
263    (app
264      (lambda unrestricted quotient1 : Nat .
265        (app
266          (lambda unrestricted quotient2 : Nat .
267            (app
268              (lambda unrestricted quotient3 : Nat .
269                (sm86Unsigned32
270                  (nat-to-byte (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
271                  (nat-to-byte (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
272                  (nat-to-byte (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
273                  (nat-to-byte (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))))
274              (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
275          (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
276      (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.