525def finishNormalizationPayload =
526 (lambda unrestricted state : (family NormalizationPayloadState) .
527 (eliminate
528 NormalizationPayloadState
529 (lambda unrestricted current : (family NormalizationPayloadState) .
530 (family NormalizationChargeResult))
531 state
532 (branch
533 NormalizationPayloadActive
534 payload
535 budget
536 .
537 (app
538 (nat-eliminate
539 (lambda unrestricted nonempty : Nat .
540 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
541 (lambda unrestricted force : Nat .
542 (constructor NormalizationChargeResult NormalizationCharged budget))
543 (lambda unrestricted predecessor : Nat .
544 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
545 (lambda unrestricted force : Nat .
546 (constructor
547 NormalizationChargeResult
548 NormalizationChargeExhausted
549 budget
550 normalizationWordOne))))
551 (nat-less-than zero (bytes-length payload)))
552 zero))
553 (branch NormalizationPayloadStopped result . result)))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.