the cycle `register` is ready at for the reader whose row `row` holds (0
when nothing is pending). The row is dispatched once per scheduling step
(sm121LowerReaderRowOf); the taken arm alone extracts its writer's entry.
1674def sm121LowerReady =
1675 (lambda unrestricted pending : (family SM121LowerPending) .
1676 (lambda unrestricted row : Nat .
1677 (lambda unrestricted register : Nat .
1678 (eliminate
1679 SM121LowerPending
1680 (lambda unrestricted current : (family SM121LowerPending) . Nat)
1681 pending
1682 (branch SM121LowerPendingEnd . zero)
1683 (branch SM121LowerPendingNext entry time class tail induction .
1684 (nat-eliminate (lambda unrestricted current : Nat . Nat)
1685 induction
1686 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (nat-add time (sm121LowerLatencyAt row (sm121LowerClassTag class)))))
1687 (nat-eliminate (lambda unrestricted current : Nat . Nat)
1688 (nat-eliminate (lambda unrestricted current : Nat . Nat)
1689 (succ zero)
1690 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
1691 (nat-less-than register entry))
1692 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
1693 (nat-less-than entry register))))))))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.