Both payloads must already be charged before this bounded product walk.
10433def workReserveCorePayloadProduct =
10434 (lambda unrestricted rows : Bytes .
10435 (lambda unrestricted columns : Bytes .
10436 (bytes-eliminate
10437 (lambda unrestricted current : Bytes .
10438 (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)))
10439 (lambda unrestricted budget : (family NormalizationBudget) .
10440 (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget))
10441 (lambda unrestricted head : Byte .
10442 (lambda unrestricted tail : Bytes .
10443 (lambda unrestricted induction : (pi unrestricted budget : (family NormalizationBudget) . (family CoreWorkResult)) .
10444 (lambda unrestricted budget : (family NormalizationBudget) .
10445 (coreWorkBind
10446 (induction budget)
10447 (lambda unrestricted ignored : (family CoreTerm) .
10448 (lambda unrestricted remaining : (family NormalizationBudget) .
10449 (coreWorkChargeBytes
10450 columns
10451 remaining
10452 (lambda unrestricted afterRow : (family NormalizationBudget) .
10453 (constructor
10454 CoreWorkResult
10455 CoreWorkCompleted
10456 (constructor CoreTerm CoreNatural)
10457 afterRow))))))))))
10458 rows)))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.