10476def workReserveCoreArithmetic =
10477 (lambda unrestricted operation : (family CoreNaturalOperation) .
10478 (lambda unrestricted left : Bytes .
10479 (lambda unrestricted right : Bytes .
10480 (lambda unrestricted budget : (family NormalizationBudget) .
10481 (eliminate
10482 CoreNaturalOperation
10483 (lambda unrestricted current : (family CoreNaturalOperation) . (family CoreWorkResult))
10484 operation
10485 (branch
10486 CoreNaturalAdd
10487 .
10488 (constructor
10489 CoreWorkResult
10490 CoreWorkCompleted
10491 (constructor CoreTerm CoreNatural)
10492 budget))
10493 (branch
10494 CoreNaturalSubtract
10495 .
10496 (constructor
10497 CoreWorkResult
10498 CoreWorkCompleted
10499 (constructor CoreTerm CoreNatural)
10500 budget))
10501 (branch
10502 CoreNaturalMultiply
10503 .
10504 (coreWorkChoose
10505 (coreNaturalAnd
10506 (nat-less-than zero (bytes-length left))
10507 (nat-less-than zero (bytes-length right)))
10508 (lambda unrestricted force : Nat .
10509 (coreWorkBind
10510 (workReserveCorePayloadProduct right left budget)
10511 (lambda unrestricted ignored : (family CoreTerm) .
10512 (lambda unrestricted remaining : (family NormalizationBudget) .
10513 (workReserveCorePayloadProduct right right remaining)))))
10514 (lambda unrestricted force : Nat .
10515 (constructor
10516 CoreWorkResult
10517 CoreWorkCompleted
10518 (constructor CoreTerm CoreNatural)
10519 budget))))
10520 (branch CoreNaturalDivide . (workReserveCoreDivision left right budget))
10521 (branch CoreNaturalModulo . (workReserveCoreDivision left right 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.