the entries still in flight at cycle `now`
381def flPrune =
382 (lambda unrestricted pending : (family ScoreboardPending) .
383 (lambda unrestricted now : Nat .
384 (eliminate ScoreboardPending (lambda unrestricted current : (family ScoreboardPending) . (family ScoreboardPending)) pending
385 (branch ScoreboardPendingEnd . (constructor ScoreboardPending ScoreboardPendingEnd))
386 (branch ScoreboardPendingNext bound ready tail induction .
387 (nat-eliminate
388 (lambda unrestricted current : Nat . (family ScoreboardPending))
389 induction
390 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardPending) .
391 (constructor ScoreboardPending ScoreboardPendingNext bound ready induction)))
392 (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.