law select_absent

bend-kit-scheduler@0.4.1.0 · queue_laws.bend:193

import bend-kit-scheduler@0.4.1.0/queue_laws.bend as QueueLaws
import Base
import bend-kit-scheduler@0.4.1.0/queue.bend as Q

193# An absent ID stays absent on every selection, in both registries. Combined
194# with cancellation above this covers any number of intervening selections.
195law select_absent:
196  for ~A: Data
197  for now: Nat
198  for +i: Nat
199  for +s: Q.State<A>
200  for eh: absent.heap(A, Q.pending(A, s), i)
201  for er: absent.list(A, Q.running(A, s), i)
202  absent.heap(A, Q.pending(A, state(A, Q.select(~A, now, s))), i) & absent.list(A, Q.running(A, state(A, Q.select(~A, now, s))), i)

Uses (19)

Used by (0)

No other definition uses this definition.