AlphaGitHub
Source/Packages

Realization.Nvidia.SM86.GreedyArgmaxSM86

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

1,985 lines222 declarations73.3 KiBSHA-256 a4ae889c3756
Download exact fileView at revision426597bda5753d86c4

def · lines 450–465

greedyArgmaxSM86Unsigned32FromNatural

Full file
450def greedyArgmaxSM86Unsigned32FromNatural =
451  (lambda unrestricted value : Nat .
452    (app
453      (lambda unrestricted quotient1 : Nat .
454        (app
455          (lambda unrestricted quotient2 : Nat .
456            (app
457              (lambda unrestricted quotient3 : Nat .
458                (sm86Unsigned32
459                  (nat-to-byte (naturalModuloUnchecked value greedyArgmaxSM86N256))
460                  (nat-to-byte (naturalModuloUnchecked quotient1 greedyArgmaxSM86N256))
461                  (nat-to-byte (naturalModuloUnchecked quotient2 greedyArgmaxSM86N256))
462                  (nat-to-byte (naturalModuloUnchecked quotient3 greedyArgmaxSM86N256))))
463              (naturalDivideUnchecked quotient2 greedyArgmaxSM86N256)))
464          (naturalDivideUnchecked quotient1 greedyArgmaxSM86N256)))
465      (naturalDivideUnchecked value greedyArgmaxSM86N256)))

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.