QueueProof.merge_all.full: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/queue_proof.bend as QueueProof
Lines 123-124 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=123&end_line=124

import Base
import bend-kit-collections@0.1.4.1/heap.bend as H
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

def merge_all.full(~A: Data, -P: Q.Ticket<A> -> Data, +a: H.Heap<Q.Ticket<A>>, +b: H.Heap<Q.Ticket<A>>, ea: L.all.heap(A, P, a), eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), a, b)):
  merge_all(~A, P, Nat.add(H.Heap.size(Q.Ticket<A>, a), H.Heap.size(Q.Ticket<A>, b)), a, b, ea, eb)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap.merge
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap.size
  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=le
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=all.heap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_all