def requeue_counter.found

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

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

398def requeue_counter.found(~A: Data, found: Maybe<&2, Q.Ticket<A>>, d: Nat, +s: Q.State<A>) -> {Q.next_id(A, L.requeue.state(A, Q.requeue.found(~A, found, d, s))) == Q.next_id(A, s) : Nat}:
399  match found:
400    case None{}:
401      {==}
402    case Some{Q.Ticket{i, old, x}}:
403      match s:
404        case Q.State{n, h, r}:
405          {==}