11098def workReduceCoreRounds =
11099 (lambda unrestricted full : Nat .
11100 (lambda unrestricted rounds : Nat .
11101 (nat-eliminate
11102 (lambda unrestricted remaining : Nat .
11103 (pi unrestricted term : (family CoreTerm) .
11104 (pi unrestricted budget : (family NormalizationBudget) . (family CoreReductionResult))))
11105 (lambda unrestricted term : (family CoreTerm) .
11106 (lambda unrestricted budget : (family NormalizationBudget) .
11107 (constructor CoreReductionResult CoreReductionExhausted term zero)))
11108 (lambda unrestricted predecessor : Nat .
11109 (lambda unrestricted induction : (pi unrestricted term : (family CoreTerm) . (pi unrestricted budget : (family NormalizationBudget) . (family CoreReductionResult))) .
11110 (lambda unrestricted term : (family CoreTerm) .
11111 (lambda unrestricted budget : (family NormalizationBudget) .
11112 (eliminate
11113 CoreWorkResult
11114 (lambda unrestricted current : (family CoreWorkResult) .
11115 (family CoreReductionResult))
11116 (workNormalizeCoreOne full term budget)
11117 (branch
11118 CoreWorkCompleted
11119 reduced
11120 remaining
11121 .
11122 (app
11123 (nat-eliminate
11124 (lambda unrestricted equal : Nat .
11125 (pi unrestricted force : Nat . (family CoreReductionResult)))
11126 (lambda unrestricted force : Nat .
11127 (countCoreReductionRound (induction reduced remaining)))
11128 (lambda unrestricted predecessor : Nat .
11129 (lambda unrestricted ignored : (pi unrestricted force : Nat . (family CoreReductionResult)) .
11130 (lambda unrestricted force : Nat .
11131 (constructor
11132 CoreReductionResult
11133 CoreReductionCompleted
11134 reduced
11135 (succ zero)))))
11136 (coreTermEqual term reduced))
11137 zero))
11138 (branch
11139 CoreWorkExhausted
11140 remaining
11141 .
11142 (constructor CoreReductionResult CoreReductionExhausted term (succ zero))))))))
11143 rounds)))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.