def requeue_ordered.found

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

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

352def requeue_ordered.found(~A: Data, found: Maybe<&2, Q.Ticket<A>>, d: Nat, +s: Q.State<A>, e: L.ordered(A, Q.pending(A, s))) -> L.ordered(A, Q.pending(A, L.requeue.state(A, Q.requeue.found(~A, found, d, s)))):
353  match found:
354    case None{}:
355      e
356    case Some{Q.Ticket{i, old, x}}:
357      match s:
358        case Q.State{n, h, r}:
359          push_ordered(~A, Q.Ticket{i, d, x}, h, e)