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 500–520

greedyArgmaxSM86ValidateVocabulary

Full file
500def greedyArgmaxSM86ValidateVocabulary =
501  (lambda unrestricted vocabulary : Nat .
502    (nat-eliminate
503      (lambda unrestricted positive : Nat . (family GreedyArgmaxSM86Validation))
504      (constructor
505        GreedyArgmaxSM86Validation
506        GreedyArgmaxSM86ValidationRejected
507        (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyZero))
508      (lambda unrestricted positivePredecessor : Nat .
509        (lambda unrestricted positiveInduction : (family GreedyArgmaxSM86Validation) .
510          (nat-eliminate
511            (lambda unrestricted bounded : Nat . (family GreedyArgmaxSM86Validation))
512            (constructor
513              GreedyArgmaxSM86Validation
514              GreedyArgmaxSM86ValidationRejected
515              (constructor GreedyArgmaxSM86FailureCode GreedyArgmaxSM86VocabularyTooLarge))
516            (lambda unrestricted boundedPredecessor : Nat .
517              (lambda unrestricted boundedInduction : (family GreedyArgmaxSM86Validation) .
518                (constructor GreedyArgmaxSM86Validation GreedyArgmaxSM86ValidationAccepted)))
519            (naturalLessOrEqual vocabulary greedyArgmaxSM86MaximumVocabulary))))
520      (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.