The payload charge bounds construction of the fold continuations. Each
demanded branch application/substitution then consumes the same remaining budget.
8407def workReduceBytesEliminateStep =
8408 (lambda unrestricted consCase : (family CoreTerm) .
8409 (lambda unrestricted head : Byte .
8410 (lambda unrestricted tail : Bytes .
8411 (lambda unrestricted induction : (family CoreTerm) .
8412 (lambda unrestricted budget : (family NormalizationBudget) .
8413 (coreWorkBind
8414 (workApplyCoreFunctionOnce
8415 consCase
8416 (constructor CoreTerm CoreByteLiteral head)
8417 budget)
8418 (lambda unrestricted withHead : (family CoreTerm) .
8419 (lambda unrestricted afterHead : (family NormalizationBudget) .
8420 (coreWorkBind
8421 (workApplyCoreFunctionOnce
8422 withHead
8423 (constructor CoreTerm CoreBytesLiteral tail)
8424 afterHead)
8425 (lambda unrestricted withTail : (family CoreTerm) .
8426 (lambda unrestricted afterTail : (family NormalizationBudget) .
8427 (workApplyCoreFunctionOnce withTail induction afterTail))))))))))))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.