9952def workFinishCoreEliminatorReduction =
9953 (lambda unrestricted familyName : Bytes .
9954 (lambda unrestricted motive : (family CoreTerm) .
9955 (lambda unrestricted scrutinee : (family CoreTerm) .
9956 (lambda unrestricted branches : (family CoreTerm) .
9957 (lambda unrestricted arguments : (family CoreTerm) .
9958 (lambda unrestricted inductionCandidates : (family CoreTerm) .
9959 (lambda unrestricted selection : (family CoreEliminatorBranchSelection) .
9960 (lambda unrestricted budget : (family NormalizationBudget) .
9961 (app
9962 (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) .
9963 (eliminate
9964 CoreEliminatorBranchSelection
9965 (lambda unrestricted current : (family CoreEliminatorBranchSelection) .
9966 (family CoreWorkResult))
9967 selection
9968 (branch
9969 CoreEliminatorBranchSelected
9970 binderCount
9971 body
9972 .
9973 (workCountCoreTermSequence
9974 arguments
9975 (lambda unrestricted argumentCount : Nat .
9976 (lambda unrestricted afterCount : (family NormalizationBudget) .
9977 (coreWorkChoose
9978 (coreNaturalAnd
9979 (nat-less-than
9980 binderCount
9981 (succ (naturalAdd argumentCount argumentCount)))
9982 (nat-less-than
9983 (nat-less-than binderCount argumentCount)
9984 (succ zero)))
9985 (lambda unrestricted force : Nat .
9986 (coreWorkBind
9987 (workReserveCoreEliminatorBookkeeping arguments afterCount)
9988 (lambda unrestricted ignored : (family CoreTerm) .
9989 (lambda unrestricted afterBookkeeping : (family NormalizationBudget) .
9990 (app
9991 (lambda unrestricted recursiveCount : Nat .
9992 (app
9993 (lambda unrestricted valueCount : Nat .
9994 (app
9995 (lambda unrestricted supplied : (family CoreTerm) .
9996 (coreWorkChoose
9997 (naturalEqual (coreTermSequenceCount supplied) binderCount)
9998 (lambda unrestricted force : Nat .
9999 (workInstantiateCoreEliminatorBranch
10000 supplied
10001 body
10002 afterBookkeeping))
10003 (lambda unrestricted force : Nat .
10004 (constructor
10005 CoreWorkResult
10006 CoreWorkCompleted
10007 (constructor
10008 CoreTerm
10009 CoreEliminator
10010 familyName
10011 motive
10012 scrutinee
10013 branches)
10014 afterBookkeeping))))
10015 (appendCoreTermSequenceForEliminator
10016 arguments
10017 (dropCoreTermSequenceForEliminator
10018 inductionCandidates
10019 valueCount))))
10020 (coreNaturalSaturatingSubtract argumentCount recursiveCount)))
10021 (coreNaturalSaturatingSubtract binderCount argumentCount))))))
10022 (lambda unrestricted force : Nat .
10023 (constructor
10024 CoreWorkResult
10025 CoreWorkCompleted
10026 (constructor
10027 CoreTerm
10028 CoreEliminator
10029 familyName
10030 motive
10031 scrutinee
10032 branches)
10033 afterCount)))))
10034 budget))
10035 (branch CoreEliminatorBranchMissing . (neutral zero))))
10036 (lambda unrestricted force : Nat .
10037 (constructor
10038 CoreWorkResult
10039 CoreWorkCompleted
10040 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
10041 budget)))))))))))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.