592def stepNormalizationNatural =
593 (lambda unrestricted target : Nat .
594 (lambda unrestricted state : (family NormalizationNaturalState) .
595 (eliminate
596 NormalizationNaturalState
597 (lambda unrestricted current : (family NormalizationNaturalState) .
598 (family NormalizationNaturalState))
599 state
600 (branch
601 NormalizationNaturalActive
602 cursor
603 budget
604 .
605 (app
606 (nat-eliminate
607 (lambda unrestricted nonempty : Nat .
608 (pi unrestricted force : Nat . (family NormalizationNaturalState)))
609 (lambda unrestricted force : Nat .
610 (constructor
611 NormalizationNaturalState
612 NormalizationNaturalStopped
613 (constructor NormalizationChargeResult NormalizationCharged budget)))
614 (lambda unrestricted predecessor : Nat .
615 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family NormalizationNaturalState)) .
616 (lambda unrestricted force : Nat .
617 (eliminate
618 NormalizationChargeResult
619 (lambda unrestricted result : (family NormalizationChargeResult) .
620 (family NormalizationNaturalState))
621 (chargeNormalizationBudgetOne budget)
622 (branch
623 NormalizationCharged
624 next
625 .
626 (constructor
627 NormalizationNaturalState
628 NormalizationNaturalActive
629 (succ cursor)
630 next))
631 (branch
632 NormalizationChargeExhausted
633 unchanged
634 amount
635 .
636 (constructor
637 NormalizationNaturalState
638 NormalizationNaturalStopped
639 (constructor
640 NormalizationChargeResult
641 NormalizationChargeExhausted
642 unchanged
643 amount)))
644 (branch
645 NormalizationChargeInvalid
646 .
647 (constructor
648 NormalizationNaturalState
649 NormalizationNaturalStopped
650 (constructor NormalizationChargeResult NormalizationChargeInvalid)))))))
651 (nat-less-than cursor target))
652 zero))
653 (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.