QueueProof.push_ordered: def of bend-kit-scheduler@0.4.1.0
Import: import bend-kit-scheduler@0.4.1.0/queue_proof.bend as QueueProof
Lines 329-330 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=329&end_line=330

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 push_ordered(~A: Data, t: Q.Ticket<A>, h: H.Heap<Q.Ticket<A>>, e: L.ordered(A, h)) -> L.ordered(A, H.Heap.push(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), t, h)):
  merge_ordered.full(~A, H.HNode{1n, t, H.HLeaf{}, H.HLeaf{}}, h, L.Both{L.Both{Unit{}, Unit{}}, L.Both{Unit{}, Unit{}}}, e)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  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.push
  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=Both
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_laws.bend&name=ordered
  https://jend.leeeet.dev/definition.txt?path=bend-kit-scheduler@0.4.1.0/queue_proof.bend&name=merge_ordered.full