10566def workReduceCoreNaturalSuccessor =
10567 (lambda unrestricted predecessor : (family CoreTerm) .
10568 (lambda unrestricted budget : (family NormalizationBudget) .
10569 (workInspectCoreNatural
10570 predecessor
10571 (lambda unrestricted digits : Bytes .
10572 (coreWorkChargeBytes
10573 digits
10574 budget
10575 (lambda unrestricted remaining : (family NormalizationBudget) .
10576 (constructor
10577 CoreWorkResult
10578 CoreWorkCompleted
10579 (reduceCoreNaturalSuccessor predecessor)
10580 remaining))))
10581 (lambda unrestricted force : Nat .
10582 (constructor
10583 CoreWorkResult
10584 CoreWorkCompleted
10585 (constructor CoreTerm CoreNaturalSuccessor predecessor)
10586 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.