the entries still in flight at cycle `now` (an entry ready by then can
raise no later stall: the program is linear in its length, not quadratic)
199def scPrune =
200 (lambda unrestricted pending : (family CompactionPending) .
201 (lambda unrestricted now : Nat .
202 (eliminate CompactionPending (lambda unrestricted current : (family CompactionPending) . (family CompactionPending)) pending
203 (branch CompactionPendingEnd . (constructor CompactionPending CompactionPendingEnd))
204 (branch CompactionPendingNext key ready tail induction .
205 (nat-eliminate (lambda unrestricted current : Nat . (family CompactionPending))
206 induction
207 (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family CompactionPending) .
208 (constructor CompactionPending CompactionPendingNext key ready induction)))
209 (naturalLess now ready))))))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.