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 1058–1066

greedyArgmaxSM86FullSlotPrograms

Full file
1058def greedyArgmaxSM86FullSlotPrograms =
1059  (lambda unrestricted count : Nat .
1060    (nat-eliminate
1061      (lambda unrestricted current : Nat . (family SM86Program))
1062      sm86ProgramEmpty
1063      (lambda unrestricted predecessor : Nat .
1064        (lambda unrestricted induction : (family SM86Program) .
1065          (sm86ProgramAppend induction (greedyArgmaxSM86FullSlotProgram predecessor))))
1066      count))

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.