AlphaGitHub
Source/Packages

Realization.Nvidia.SM86.GreedyArgmaxSM86

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

1,978 lines222 declarations72.8 KiBSHA-256 b399c7cf28cc
Download exact fileView at revisionf5034773ad4bb52133

def · lines 443–458

greedyArgmaxSM86Unsigned32FromNatural

Full file
443def greedyArgmaxSM86Unsigned32FromNatural =
444  (lambda unrestricted value : Nat .
445    (app
446      (lambda unrestricted quotient1 : Nat .
447        (app
448          (lambda unrestricted quotient2 : Nat .
449            (app
450              (lambda unrestricted quotient3 : Nat .
451                (sm86Unsigned32
452                  (nat-to-byte (naturalModuloUnchecked value greedyArgmaxSM86N256))
453                  (nat-to-byte (naturalModuloUnchecked quotient1 greedyArgmaxSM86N256))
454                  (nat-to-byte (naturalModuloUnchecked quotient2 greedyArgmaxSM86N256))
455                  (nat-to-byte (naturalModuloUnchecked quotient3 greedyArgmaxSM86N256))))
456              (naturalDivideUnchecked quotient2 greedyArgmaxSM86N256)))
457          (naturalDivideUnchecked quotient1 greedyArgmaxSM86N256)))
458      (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.