655def repeatNormalizationNaturalSmall =
656 (lambda unrestricted count : Nat .
657 (lambda unrestricted step : (pi unrestricted state : (family NormalizationNaturalState) . (family NormalizationNaturalState)) .
658 (lambda unrestricted state : (family NormalizationNaturalState) .
659 (eliminate
660 NormalizationNaturalState
661 (lambda unrestricted current : (family NormalizationNaturalState) .
662 (family NormalizationNaturalState))
663 state
664 (branch
665 NormalizationNaturalActive
666 cursor
667 budget
668 .
669 (nat-eliminate
670 (lambda unrestricted index : Nat . (family NormalizationNaturalState))
671 state
672 (lambda unrestricted predecessor : Nat .
673 (lambda unrestricted induction : (family NormalizationNaturalState) .
674 (step induction)))
675 count))
676 (branch NormalizationNaturalStopped 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.