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 507–527

greedyArgmaxSM86ValidateVocabulary

Full file
507def greedyArgmaxSM86ValidateVocabulary =
508  (lambda unrestricted vocabulary : Nat .
509    (nat-eliminate
510      (lambda unrestricted positive : Nat . (family GreedyArgmaxSM86Validation))
511      (constructor
512        GreedyArgmaxSM86Validation
513        GreedyArgmaxSM86ValidationRejected
514        (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyZero))
515      (lambda unrestricted positivePredecessor : Nat .
516        (lambda unrestricted positiveInduction : (family GreedyArgmaxSM86Validation) .
517          (nat-eliminate
518            (lambda unrestricted bounded : Nat . (family GreedyArgmaxSM86Validation))
519            (constructor
520              GreedyArgmaxSM86Validation
521              GreedyArgmaxSM86ValidationRejected
522              (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyTooLarge))
523            (lambda unrestricted boundedPredecessor : Nat .
524              (lambda unrestricted boundedInduction : (family GreedyArgmaxSM86Validation) .
525                (constructor GreedyArgmaxSM86Validation GreedyArgmaxSM86ValidationAccepted)))
526            (naturalLessOrEqual vocabulary greedyArgmaxSM86MaximumVocabulary))))
527      (naturalNonzero vocabulary)))

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.