QueueProof.take_equivalent.step: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/queue_proof.bend as QueueProof
Lines 15-20 of bend-kit-scheduler@0.4.1.0/queue_proof.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&start_line=15&end_line=20

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

def take_equivalent.step(-A: Data, b: Bool, t: Q.Ticket<A>, rest: List<&2, Q.Ticket<A>>, found: Maybe<&2, Q.Ticket<A>>) -> {Q.take.keep(A, b, t, Q.Taken{rest, found}) == Q.Taken{Q.remove.list.keep(A, b, t, rest), Q.find.list.choose(A, b, t, found)} : Q.Taken<A>}:
  match b:
    case True{}:
      {==}
    case False{}:
      {==}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=Taken
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=Ticket
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=find.list.choose
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=remove.list.keep
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue.bend&name=take.keep