5010def finishCoreEliminatorReduction =
5011 (lambda unrestricted familyName : Bytes .
5012 (lambda unrestricted motive : (family CoreTerm) .
5013 (lambda unrestricted scrutinee : (family CoreTerm) .
5014 (lambda unrestricted branches : (family CoreTerm) .
5015 (lambda unrestricted arguments : (family CoreTerm) .
5016 (lambda unrestricted inductionCandidates : (family CoreTerm) .
5017 (lambda unrestricted selection : (family CoreEliminatorBranchSelection) .
5018 (eliminate
5019 CoreEliminatorBranchSelection
5020 (lambda unrestricted value : (family CoreEliminatorBranchSelection) .
5021 (family CoreTerm))
5022 selection
5023 (branch
5024 CoreEliminatorBranchSelected
5025 binderCount
5026 body
5027 .
5028 (app
5029 (lambda unrestricted argumentCount : Nat .
5030 (app
5031 (lambda unrestricted recursiveCount : Nat .
5032 (app
5033 (lambda unrestricted valueCount : Nat .
5034 (app
5035 (lambda unrestricted inductionResults : (family CoreTerm) .
5036 (app
5037 (lambda unrestricted supplied : (family CoreTerm) .
5038 (nat-eliminate
5039 (lambda unrestricted arityMatches : Nat . (family CoreTerm))
5040 (constructor
5041 CoreTerm
5042 CoreEliminator
5043 familyName
5044 motive
5045 scrutinee
5046 branches)
5047 (lambda unrestricted predecessor : Nat .
5048 (lambda unrestricted induction : (family CoreTerm) .
5049 (instantiateCoreEliminatorBranch supplied body)))
5050 (naturalEqual (coreTermSequenceCount supplied) binderCount)))
5051 (appendCoreTermSequenceForEliminator
5052 arguments
5053 inductionResults)))
5054 (dropCoreTermSequenceForEliminator inductionCandidates valueCount)))
5055 (coreNaturalSaturatingSubtract argumentCount recursiveCount)))
5056 (coreNaturalSaturatingSubtract binderCount argumentCount)))
5057 (coreTermSequenceCount arguments)))
5058 (branch
5059 CoreEliminatorBranchMissing
5060 .
5061 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))))))))))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.