10641def workNormalizeCoreOne =
10642 (lambda unrestricted full : Nat .
10643 (lambda unrestricted term : (family CoreTerm) .
10644 (eliminate
10645 CoreTerm
10646 (lambda unrestricted current : (family CoreTerm) .
10647 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))
10648 term
10649 (branch
10650 CoreUniverse
10651 coreUniverseLevel
10652 .
10653 (lambda unrestricted budget : (family NormalizationBudget) .
10654 (coreWorkCharge
10655 coreWorkOne
10656 budget
10657 (lambda unrestricted remaining : (family NormalizationBudget) .
10658 (constructor
10659 CoreWorkResult
10660 CoreWorkCompleted
10661 (constructor CoreTerm CoreUniverse coreUniverseLevel)
10662 remaining)))))
10663 (branch
10664 CoreNatural
10665 .
10666 (lambda unrestricted budget : (family NormalizationBudget) .
10667 (coreWorkCharge
10668 coreWorkOne
10669 budget
10670 (lambda unrestricted remaining : (family NormalizationBudget) .
10671 (constructor
10672 CoreWorkResult
10673 CoreWorkCompleted
10674 (constructor CoreTerm CoreNatural)
10675 remaining)))))
10676 (branch
10677 CoreNaturalLiteral
10678 coreNaturalValue
10679 .
10680 (lambda unrestricted budget : (family NormalizationBudget) .
10681 (coreWorkCharge
10682 coreWorkOne
10683 budget
10684 (lambda unrestricted remaining : (family NormalizationBudget) .
10685 (constructor
10686 CoreWorkResult
10687 CoreWorkCompleted
10688 (constructor CoreTerm CoreNaturalLiteral coreNaturalValue)
10689 remaining)))))
10690 (branch
10691 CoreBound
10692 coreBoundIndex
10693 .
10694 (lambda unrestricted budget : (family NormalizationBudget) .
10695 (coreWorkCharge
10696 coreWorkOne
10697 budget
10698 (lambda unrestricted remaining : (family NormalizationBudget) .
10699 (constructor
10700 CoreWorkResult
10701 CoreWorkCompleted
10702 (constructor CoreTerm CoreBound coreBoundIndex)
10703 remaining)))))
10704 (branch
10705 CorePi
10706 corePiMultiplicity
10707 corePiDomain
10708 corePiCodomain
10709 ih_corePiDomain
10710 ih_corePiCodomain
10711 .
10712 (lambda unrestricted budget : (family NormalizationBudget) .
10713 (coreWorkCharge
10714 coreWorkOne
10715 budget
10716 (lambda unrestricted remaining : (family NormalizationBudget) .
10717 (coreWorkBind
10718 (ih_corePiDomain remaining)
10719 (lambda unrestricted new_corePiDomain : (family CoreTerm) .
10720 (lambda unrestricted remaining : (family NormalizationBudget) .
10721 (coreWorkBind
10722 (ih_corePiCodomain remaining)
10723 (lambda unrestricted new_corePiCodomain : (family CoreTerm) .
10724 (lambda unrestricted remaining : (family NormalizationBudget) .
10725 (constructor
10726 CoreWorkResult
10727 CoreWorkCompleted
10728 (constructor
10729 CoreTerm
10730 CorePi
10731 corePiMultiplicity
10732 new_corePiDomain
10733 new_corePiCodomain)
10734 remaining)))))))))))
10735 (branch
10736 CoreLambda
10737 coreLambdaMultiplicity
10738 coreLambdaDomain
10739 coreLambdaBody
10740 ih_coreLambdaDomain
10741 ih_coreLambdaBody
10742 .
10743 (lambda unrestricted budget : (family NormalizationBudget) .
10744 (coreWorkCharge
10745 coreWorkOne
10746 budget
10747 (lambda unrestricted remaining : (family NormalizationBudget) .
10748 (coreWorkBind
10749 (ih_coreLambdaDomain remaining)
10750 (lambda unrestricted new_coreLambdaDomain : (family CoreTerm) .
10751 (lambda unrestricted remaining : (family NormalizationBudget) .
10752 (coreWorkBind
10753 (ih_coreLambdaBody remaining)
10754 (lambda unrestricted new_coreLambdaBody : (family CoreTerm) .
10755 (lambda unrestricted remaining : (family NormalizationBudget) .
10756 (constructor
10757 CoreWorkResult
10758 CoreWorkCompleted
10759 (constructor
10760 CoreTerm
10761 CoreLambda
10762 coreLambdaMultiplicity
10763 new_coreLambdaDomain
10764 new_coreLambdaBody)
10765 remaining)))))))))))
10766 (branch
10767 CoreLet
10768 coreLetMultiplicity
10769 coreLetAnnotation
10770 coreLetValue
10771 coreLetBody
10772 ih_coreLetAnnotation
10773 ih_coreLetValue
10774 ih_coreLetBody
10775 .
10776 (lambda unrestricted budget : (family NormalizationBudget) .
10777 (coreWorkCharge
10778 coreWorkOne
10779 budget
10780 (lambda unrestricted remaining : (family NormalizationBudget) .
10781 (coreWorkBind
10782 (ih_coreLetValue remaining)
10783 (lambda unrestricted new_coreLetValue : (family CoreTerm) .
10784 (lambda unrestricted remaining : (family NormalizationBudget) .
10785 (coreWorkBind
10786 (ih_coreLetBody remaining)
10787 (lambda unrestricted new_coreLetBody : (family CoreTerm) .
10788 (lambda unrestricted remaining : (family NormalizationBudget) .
10789 (workSubstituteCoreTop new_coreLetValue new_coreLetBody remaining)))))))))))
10790 (branch
10791 CoreApplication
10792 coreApplicationFunction
10793 coreApplicationArgument
10794 ih_coreApplicationFunction
10795 ih_coreApplicationArgument
10796 .
10797 (lambda unrestricted budget : (family NormalizationBudget) .
10798 (coreWorkCharge
10799 coreWorkOne
10800 budget
10801 (lambda unrestricted remaining : (family NormalizationBudget) .
10802 (coreWorkBind
10803 (ih_coreApplicationFunction remaining)
10804 (lambda unrestricted new_coreApplicationFunction : (family CoreTerm) .
10805 (lambda unrestricted remaining : (family NormalizationBudget) .
10806 (coreWorkBind
10807 (ih_coreApplicationArgument remaining)
10808 (lambda unrestricted new_coreApplicationArgument : (family CoreTerm) .
10809 (lambda unrestricted remaining : (family NormalizationBudget) .
10810 (coreWorkChoose
10811 full
10812 (lambda unrestricted force : Nat .
10813 (workReduceCoreApplication
10814 new_coreApplicationFunction
10815 new_coreApplicationArgument
10816 remaining))
10817 (lambda unrestricted force : Nat .
10818 (workApplyCoreFunctionOnce
10819 new_coreApplicationFunction
10820 new_coreApplicationArgument
10821 remaining)))))))))))))
10822 (branch
10823 CoreNaturalArithmetic
10824 coreArithmeticOperation
10825 coreArithmeticLeft
10826 coreArithmeticRight
10827 ih_coreArithmeticLeft
10828 ih_coreArithmeticRight
10829 .
10830 (lambda unrestricted budget : (family NormalizationBudget) .
10831 (coreWorkCharge
10832 coreWorkOne
10833 budget
10834 (lambda unrestricted remaining : (family NormalizationBudget) .
10835 (coreWorkBind
10836 (ih_coreArithmeticLeft remaining)
10837 (lambda unrestricted new_coreArithmeticLeft : (family CoreTerm) .
10838 (lambda unrestricted remaining : (family NormalizationBudget) .
10839 (coreWorkBind
10840 (ih_coreArithmeticRight remaining)
10841 (lambda unrestricted new_coreArithmeticRight : (family CoreTerm) .
10842 (lambda unrestricted remaining : (family NormalizationBudget) .
10843 (workReduceCoreArithmetic
10844 coreArithmeticOperation
10845 new_coreArithmeticLeft
10846 new_coreArithmeticRight
10847 remaining)))))))))))
10848 (branch
10849 CoreNaturalSuccessor
10850 coreNaturalPredecessor
10851 ih_coreNaturalPredecessor
10852 .
10853 (lambda unrestricted budget : (family NormalizationBudget) .
10854 (coreWorkCharge
10855 coreWorkOne
10856 budget
10857 (lambda unrestricted remaining : (family NormalizationBudget) .
10858 (coreWorkBind
10859 (ih_coreNaturalPredecessor remaining)
10860 (lambda unrestricted new_coreNaturalPredecessor : (family CoreTerm) .
10861 (lambda unrestricted remaining : (family NormalizationBudget) .
10862 (workReduceCoreNaturalSuccessor new_coreNaturalPredecessor remaining))))))))
10863 (branch
10864 CoreByte
10865 .
10866 (lambda unrestricted budget : (family NormalizationBudget) .
10867 (coreWorkCharge
10868 coreWorkOne
10869 budget
10870 (lambda unrestricted remaining : (family NormalizationBudget) .
10871 (constructor
10872 CoreWorkResult
10873 CoreWorkCompleted
10874 (constructor CoreTerm CoreByte)
10875 remaining)))))
10876 (branch
10877 CoreByteLiteral
10878 coreByteValue
10879 .
10880 (lambda unrestricted budget : (family NormalizationBudget) .
10881 (coreWorkCharge
10882 coreWorkOne
10883 budget
10884 (lambda unrestricted remaining : (family NormalizationBudget) .
10885 (constructor
10886 CoreWorkResult
10887 CoreWorkCompleted
10888 (constructor CoreTerm CoreByteLiteral coreByteValue)
10889 remaining)))))
10890 (branch
10891 CoreBytes
10892 .
10893 (lambda unrestricted budget : (family NormalizationBudget) .
10894 (coreWorkCharge
10895 coreWorkOne
10896 budget
10897 (lambda unrestricted remaining : (family NormalizationBudget) .
10898 (constructor
10899 CoreWorkResult
10900 CoreWorkCompleted
10901 (constructor CoreTerm CoreBytes)
10902 remaining)))))
10903 (branch
10904 CoreBytesLiteral
10905 coreBytesValue
10906 .
10907 (lambda unrestricted budget : (family NormalizationBudget) .
10908 (coreWorkCharge
10909 coreWorkOne
10910 budget
10911 (lambda unrestricted remaining : (family NormalizationBudget) .
10912 (constructor
10913 CoreWorkResult
10914 CoreWorkCompleted
10915 (constructor CoreTerm CoreBytesLiteral coreBytesValue)
10916 remaining)))))
10917 (branch
10918 CorePrimitiveTerm
10919 corePrimitive
10920 .
10921 (lambda unrestricted budget : (family NormalizationBudget) .
10922 (coreWorkCharge
10923 coreWorkOne
10924 budget
10925 (lambda unrestricted remaining : (family NormalizationBudget) .
10926 (constructor
10927 CoreWorkResult
10928 CoreWorkCompleted
10929 (constructor CoreTerm CorePrimitiveTerm corePrimitive)
10930 remaining)))))
10931 (branch
10932 CoreTermSequenceEnd
10933 .
10934 (lambda unrestricted budget : (family NormalizationBudget) .
10935 (coreWorkCharge
10936 coreWorkOne
10937 budget
10938 (lambda unrestricted remaining : (family NormalizationBudget) .
10939 (constructor
10940 CoreWorkResult
10941 CoreWorkCompleted
10942 (constructor CoreTerm CoreTermSequenceEnd)
10943 remaining)))))
10944 (branch
10945 CoreTermSequenceNext
10946 coreTermSequenceHead
10947 coreTermSequenceTail
10948 ih_coreTermSequenceHead
10949 ih_coreTermSequenceTail
10950 .
10951 (lambda unrestricted budget : (family NormalizationBudget) .
10952 (coreWorkCharge
10953 coreWorkOne
10954 budget
10955 (lambda unrestricted remaining : (family NormalizationBudget) .
10956 (coreWorkBind
10957 (ih_coreTermSequenceHead remaining)
10958 (lambda unrestricted new_coreTermSequenceHead : (family CoreTerm) .
10959 (lambda unrestricted remaining : (family NormalizationBudget) .
10960 (coreWorkBind
10961 (ih_coreTermSequenceTail remaining)
10962 (lambda unrestricted new_coreTermSequenceTail : (family CoreTerm) .
10963 (lambda unrestricted remaining : (family NormalizationBudget) .
10964 (constructor
10965 CoreWorkResult
10966 CoreWorkCompleted
10967 (constructor
10968 CoreTerm
10969 CoreTermSequenceNext
10970 new_coreTermSequenceHead
10971 new_coreTermSequenceTail)
10972 remaining)))))))))))
10973 (branch
10974 CoreFamilyApplication
10975 coreFamilyName
10976 coreFamilyArguments
10977 ih_coreFamilyArguments
10978 .
10979 (lambda unrestricted budget : (family NormalizationBudget) .
10980 (coreWorkCharge
10981 coreWorkOne
10982 budget
10983 (lambda unrestricted remaining : (family NormalizationBudget) .
10984 (coreWorkBind
10985 (ih_coreFamilyArguments remaining)
10986 (lambda unrestricted new_coreFamilyArguments : (family CoreTerm) .
10987 (lambda unrestricted remaining : (family NormalizationBudget) .
10988 (constructor
10989 CoreWorkResult
10990 CoreWorkCompleted
10991 (constructor
10992 CoreTerm
10993 CoreFamilyApplication
10994 coreFamilyName
10995 new_coreFamilyArguments)
10996 remaining))))))))
10997 (branch
10998 CoreConstructorApplication
10999 coreConstructorFamilyName
11000 coreConstructorName
11001 coreConstructorArguments
11002 ih_coreConstructorArguments
11003 .
11004 (lambda unrestricted budget : (family NormalizationBudget) .
11005 (coreWorkCharge
11006 coreWorkOne
11007 budget
11008 (lambda unrestricted remaining : (family NormalizationBudget) .
11009 (coreWorkBind
11010 (ih_coreConstructorArguments remaining)
11011 (lambda unrestricted new_coreConstructorArguments : (family CoreTerm) .
11012 (lambda unrestricted remaining : (family NormalizationBudget) .
11013 (constructor
11014 CoreWorkResult
11015 CoreWorkCompleted
11016 (constructor
11017 CoreTerm
11018 CoreConstructorApplication
11019 coreConstructorFamilyName
11020 coreConstructorName
11021 new_coreConstructorArguments)
11022 remaining))))))))
11023 (branch
11024 CoreEliminatorBranch
11025 coreBranchConstructorName
11026 coreBranchBinderCount
11027 coreBranchBody
11028 ih_coreBranchBody
11029 .
11030 (lambda unrestricted budget : (family NormalizationBudget) .
11031 (coreWorkCharge
11032 coreWorkOne
11033 budget
11034 (lambda unrestricted remaining : (family NormalizationBudget) .
11035 (coreWorkBind
11036 (ih_coreBranchBody remaining)
11037 (lambda unrestricted new_coreBranchBody : (family CoreTerm) .
11038 (lambda unrestricted remaining : (family NormalizationBudget) .
11039 (constructor
11040 CoreWorkResult
11041 CoreWorkCompleted
11042 (constructor
11043 CoreTerm
11044 CoreEliminatorBranch
11045 coreBranchConstructorName
11046 coreBranchBinderCount
11047 new_coreBranchBody)
11048 remaining))))))))
11049 (branch
11050 CoreEliminator
11051 coreEliminatedFamilyName
11052 coreEliminatorMotive
11053 coreEliminatorScrutinee
11054 coreEliminatorBranches
11055 ih_coreEliminatorMotive
11056 ih_coreEliminatorScrutinee
11057 ih_coreEliminatorBranches
11058 .
11059 (lambda unrestricted budget : (family NormalizationBudget) .
11060 (coreWorkCharge
11061 coreWorkOne
11062 budget
11063 (lambda unrestricted remaining : (family NormalizationBudget) .
11064 (coreWorkBind
11065 (ih_coreEliminatorMotive remaining)
11066 (lambda unrestricted new_coreEliminatorMotive : (family CoreTerm) .
11067 (lambda unrestricted remaining : (family NormalizationBudget) .
11068 (coreWorkBind
11069 (ih_coreEliminatorScrutinee remaining)
11070 (lambda unrestricted new_coreEliminatorScrutinee : (family CoreTerm) .
11071 (lambda unrestricted remaining : (family NormalizationBudget) .
11072 (coreWorkBind
11073 (ih_coreEliminatorBranches remaining)
11074 (lambda unrestricted new_coreEliminatorBranches : (family CoreTerm) .
11075 (lambda unrestricted remaining : (family NormalizationBudget) .
11076 (coreWorkChoose
11077 full
11078 (lambda unrestricted force : Nat .
11079 (workReduceCoreGenericEliminator
11080 coreEliminatedFamilyName
11081 new_coreEliminatorMotive
11082 new_coreEliminatorScrutinee
11083 new_coreEliminatorBranches
11084 remaining))
11085 (lambda unrestricted force : Nat .
11086 (constructor
11087 CoreWorkResult
11088 CoreWorkCompleted
11089 (constructor
11090 CoreTerm
11091 CoreEliminator
11092 coreEliminatedFamilyName
11093 new_coreEliminatorMotive
11094 new_coreEliminatorScrutinee
11095 new_coreEliminatorBranches)
11096 remaining)))))))))))))))))))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.