708def finishNormalizationNatural =
709 (lambda unrestricted target : Nat .
710 (lambda unrestricted state : (family NormalizationNaturalState) .
711 (eliminate
712 NormalizationNaturalState
713 (lambda unrestricted current : (family NormalizationNaturalState) .
714 (family NormalizationChargeResult))
715 state
716 (branch
717 NormalizationNaturalActive
718 cursor
719 budget
720 .
721 (app
722 (nat-eliminate
723 (lambda unrestricted nonempty : Nat .
724 (pi unrestricted force : Nat . (family NormalizationChargeResult)))
725 (lambda unrestricted force : Nat .
726 (constructor NormalizationChargeResult NormalizationCharged budget))
727 (lambda unrestricted predecessor : Nat .
728 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationChargeResult)) .
729 (lambda unrestricted force : Nat .
730 (constructor
731 NormalizationChargeResult
732 NormalizationChargeExhausted
733 budget
734 normalizationWordOne))))
735 (nat-less-than cursor target))
736 zero))
737 (branch NormalizationNaturalStopped 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.