10523def workReduceCoreArithmetic =
10524 (lambda unrestricted operation : (family CoreNaturalOperation) .
10525 (lambda unrestricted left : (family CoreTerm) .
10526 (lambda unrestricted right : (family CoreTerm) .
10527 (lambda unrestricted budget : (family NormalizationBudget) .
10528 (app
10529 (lambda unrestricted neutral : (pi unrestricted force : Nat . (family CoreWorkResult)) .
10530 (workInspectCoreNatural
10531 left
10532 (lambda unrestricted leftDigits : Bytes .
10533 (workInspectCoreNatural
10534 right
10535 (lambda unrestricted rightDigits : Bytes .
10536 (coreWorkChargeBytes
10537 leftDigits
10538 budget
10539 (lambda unrestricted afterLeft : (family NormalizationBudget) .
10540 (coreWorkChargeBytes
10541 rightDigits
10542 afterLeft
10543 (lambda unrestricted afterRight : (family NormalizationBudget) .
10544 (coreWorkBind
10545 (workReserveCoreArithmetic
10546 operation
10547 leftDigits
10548 rightDigits
10549 afterRight)
10550 (lambda unrestricted ignored : (family CoreTerm) .
10551 (lambda unrestricted remaining : (family NormalizationBudget) .
10552 (constructor
10553 CoreWorkResult
10554 CoreWorkCompleted
10555 (reduceCoreArithmetic operation left right)
10556 remaining)))))))))
10557 neutral))
10558 neutral))
10559 (lambda unrestricted force : Nat .
10560 (constructor
10561 CoreWorkResult
10562 CoreWorkCompleted
10563 (constructor CoreTerm CoreNaturalArithmetic operation left right)
10564 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.