AlphaGitHub
Source/Packages

Compiler.NormalizationBudget

packages/compiler/src/Compiler/NormalizationBudget.alpha

775 lines53 declarations32.9 KiBSHA-256 582a37dd050a
Download exact fileView at revisionf5034773ad4bb52133

def · lines 472–493

repeatNormalizationPayloadSmall

Full file
472def repeatNormalizationPayloadSmall =
473  (lambda unrestricted count : Nat .
474    (lambda unrestricted step : (pi unrestricted state : (family NormalizationPayloadState) . (family NormalizationPayloadState)) .
475      (lambda unrestricted state : (family NormalizationPayloadState) .
476        (eliminate
477          NormalizationPayloadState
478          (lambda unrestricted current : (family NormalizationPayloadState) .
479            (family NormalizationPayloadState))
480          state
481          (branch
482            NormalizationPayloadActive
483            payload
484            budget
485            .
486            (nat-eliminate
487              (lambda unrestricted index : Nat . (family NormalizationPayloadState))
488              state
489              (lambda unrestricted predecessor : Nat .
490                (lambda unrestricted induction : (family NormalizationPayloadState) .
491                  (step induction)))
492              count))
493          (branch NormalizationPayloadStopped result . state)))))

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.