10460def workReserveCoreDivision =
10461 (lambda unrestricted left : Bytes .
10462 (lambda unrestricted right : Bytes .
10463 (lambda unrestricted budget : (family NormalizationBudget) .
10464 (nat-eliminate
10465 (lambda unrestricted current : Nat . (family CoreWorkResult))
10466 (constructor CoreWorkResult CoreWorkCompleted (constructor CoreTerm CoreNatural) budget)
10467 (lambda unrestricted predecessor : Nat .
10468 (lambda unrestricted induction : (family CoreWorkResult) .
10469 (coreWorkBind
10470 induction
10471 (lambda unrestricted ignored : (family CoreTerm) .
10472 (lambda unrestricted remaining : (family NormalizationBudget) .
10473 (workReserveCorePayloadProduct left right remaining))))))
10474 (byte-to-nat (byte 9))))))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.