def requeue_absent

bend-kit-scheduler@0.4.1.0 · queue_proof.bend:258

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

258def requeue_absent(~A: Data, +i: Nat, d: Nat, +s: Q.State<A>, e: {Q.find.list(A, Q.running(A, s), i) == None{} : Maybe<&2, Q.Ticket<A>>}) -> {L.requeued(A, Q.requeue(~A, i, d, s)) == False{} : Bool}:
259  match s:
260    case Q.State{n, h, r}:
261      %Equal.sym(Q.State<A> & Bool, Q.requeue(~A, i, d, Q.State{n, h, r}), L.requeue.reference(~A, i, d, Q.State{n, h, r}), L.requeue_equivalent(~A, i, d, Q.State{n, h, r})) : {L.requeued(A, _) == False{} : Bool}
262      %Equal.sym(Maybe<&2, Q.Ticket<A>>, Q.find.list(A, r, i), None{}, e) : {L.requeued(A, Q.requeue.completed(~A, (Q.State{n, h, Q.remove.list(A, r, i)}, _), d)) == False{} : Bool}
263      {==}