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 1061–1080

greedyArgmaxSM86SlotPrograms

Full file
1061def greedyArgmaxSM86SlotPrograms =
1062  (lambda unrestricted vocabulary : Nat .
1063    (app
1064      (lambda unrestricted fullSlots : Nat .
1065        (app
1066          (lambda unrestricted remainder : Nat .
1067            (app
1068              (lambda unrestricted fullProgram : (family SM86Program) .
1069                (nat-eliminate
1070                  (lambda unrestricted tailLanes : Nat . (family SM86Program))
1071                  fullProgram
1072                  (lambda unrestricted lastLane : Nat .
1073                    (lambda unrestricted tailInduction : (family SM86Program) .
1074                      (sm86ProgramAppend
1075                        fullProgram
1076                        (greedyArgmaxSM86PartialSlotProgram fullSlots lastLane))))
1077                  remainder))
1078              (greedyArgmaxSM86FullSlotPrograms fullSlots)))
1079          (naturalModuloUnchecked vocabulary greedyArgmaxSM86N256)))
1080      (naturalDivideUnchecked vocabulary 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.