Every composed block checks for exhaustion before entering its inner loop.
7536def repeatCoreNaturalWorkSmall =
7537 (lambda unrestricted count : Nat .
7538 (lambda unrestricted step : (pi unrestricted state : (family CoreNaturalWorkState) . (family CoreNaturalWorkState)) .
7539 (lambda unrestricted state : (family CoreNaturalWorkState) .
7540 (eliminate
7541 CoreNaturalWorkState
7542 (lambda unrestricted current : (family CoreNaturalWorkState) .
7543 (family CoreNaturalWorkState))
7544 state
7545 (branch
7546 CoreNaturalWorkActive
7547 predecessor
7548 term
7549 budget
7550 .
7551 (nat-eliminate
7552 (lambda unrestricted index : Nat . (family CoreNaturalWorkState))
7553 state
7554 (lambda unrestricted predecessor : Nat .
7555 (lambda unrestricted induction : (family CoreNaturalWorkState) . (step induction)))
7556 count))
7557 (branch CoreNaturalWorkStopped budget . state)))))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.