Part of `elaborateClosedNatural`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
596def elaborateClosedNaturalPart1 =
597 (lambda unrestricted function : (family Term) .
598 (lambda unrestricted ih_function : (family ClosedNaturalElaboration) .
599 (lambda unrestricted ih_argument : (family ClosedNaturalElaboration) .
600 (eliminate
601 Term
602 (lambda unrestricted value : (family Term) . (family ClosedNaturalElaboration))
603 function
604 (branch Variable spelling . (elaboratePrimitiveApplication spelling ih_argument))
605 (branch Universe level . (applyElaboratedFunction ih_function ih_argument))
606 (branch NaturalType . (applyElaboratedFunction ih_function ih_argument))
607 (branch NaturalZero . (applyElaboratedFunction ih_function ih_argument))
608 (branch
609 NaturalLiteral
610 naturalLiteralValue
611 .
612 (applyElaboratedFunction ih_function ih_argument))
613 (branch
614 NaturalSuccessor
615 predecessor
616 ih_predecessor
617 .
618 (applyElaboratedFunction ih_function ih_argument))
619 (branch
620 Application
621 nestedFunction
622 nestedArgument
623 ih_nestedFunction
624 ih_nestedArgument
625 .
626 (applyElaboratedFunction ih_function ih_argument))
627 (branch
628 NaturalArithmetic
629 operation
630 nestedFunction
631 nestedArgument
632 ih_nestedFunction
633 ih_nestedArgument
634 .
635 unsupportedApplicationResult)
636 (branch
637 Lambda
638 quantityTag
639 binderSpelling
640 domain
641 body
642 ih_domain
643 ih_body
644 .
645 (applyElaboratedFunction ih_function ih_argument))
646 (branch
647 Pi
648 quantityTag
649 binderSpelling
650 domain
651 codomain
652 ih_domain
653 ih_codomain
654 .
655 (applyElaboratedFunction ih_function ih_argument))
656 (branch BytesType . (applyElaboratedFunction ih_function ih_argument))
657 (branch BytesLiteral bytesValue . (applyElaboratedFunction ih_function ih_argument))
658 (branch ByteType . (applyElaboratedFunction ih_function ih_argument))
659 (branch ByteLiteral byteValue . (applyElaboratedFunction ih_function ih_argument))
660 (branch TermSequenceEnd . (applyElaboratedFunction ih_function ih_argument))
661 (branch
662 TermSequenceNext
663 sequenceHead
664 sequenceTail
665 ih_sequenceHead
666 ih_sequenceTail
667 .
668 (applyElaboratedFunction ih_function ih_argument))
669 (branch
670 TermEliminatorBranch
671 constructorSpelling
672 binderNames
673 body
674 ih_binderNames
675 ih_body
676 .
677 (applyElaboratedFunction ih_function ih_argument))
678 (branch
679 FamilyApplication
680 familySpelling
681 familyArguments
682 ih_familyArguments
683 .
684 (applyElaboratedFunction ih_function ih_argument))
685 (branch
686 ConstructorApplication
687 familySpelling
688 constructorSpelling
689 constructorArguments
690 ih_constructorArguments
691 .
692 (applyElaboratedFunction ih_function ih_argument))
693 (branch
694 Eliminator
695 eliminatedFamilySpelling
696 motive
697 scrutinee
698 branches
699 ih_motive
700 ih_scrutinee
701 ih_branches
702 .
703 (applyElaboratedFunction ih_function ih_argument))
704 (branch
705 Match
706 family
707 scrutinee
708 branches
709 ih_scrutinee
710 ih_branches
711 .
712 (applyElaboratedFunction ih_function ih_argument))
713 (branch
714 MatchWith
715 family
716 motive
717 scrutinee
718 branches
719 ih_motive
720 ih_scrutinee
721 ih_branches
722 .
723 (applyElaboratedFunction ih_function ih_argument))
724 (branch IntegerLiteral spelling . (applyElaboratedFunction ih_function ih_argument))
725 (branch
726 RecordConstruction
727 name
728 origin
729 bindings
730 ih_bindings
731 .
732 (applyElaboratedFunction ih_function ih_argument))
733 (branch
734 RecordAssignment
735 name
736 origin
737 value
738 ih_value
739 .
740 (applyElaboratedFunction ih_function ih_argument))
741 (branch
742 RecordProjection
743 name
744 field
745 origin
746 value
747 ih_value
748 .
749 (applyElaboratedFunction ih_function ih_argument))
750 (branch
751 RecordUpdate
752 name
753 origin
754 value
755 bindings
756 ih_value
757 ih_bindings
758 .
759 (applyElaboratedFunction ih_function ih_argument))
760 (branch
761 LocalLet
762 quantity
763 binder
764 hasAnnotation
765 annotation
766 value
767 body
768 ih_annotation
769 ih_value
770 ih_body
771 .
772 (applyElaboratedFunction ih_function ih_argument))
773 (branch
774 DoBlock
775 effects
776 result
777 body
778 ih_effects
779 ih_result
780 ih_body
781 .
782 (applyElaboratedFunction ih_function ih_argument))
783 (branch
784 DoStep
785 named
786 quantity
787 binder
788 computation
789 continuation
790 ih_computation
791 ih_continuation
792 .
793 (applyElaboratedFunction ih_function ih_argument))
794 (branch DoReturn value ih_value . (applyElaboratedFunction ih_function ih_argument))))))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.