BinaryHeap.pop_with: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/containers/binary_heap.bend as BinaryHeap
Lines 261-272 of bend-collections@1.0.0.0/src/containers/binary_heap.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/containers/binary_heap.bend&start_line=261&end_line=272

import Base
import bend-collections@1.0.0.0/src/containers/types/binary_heap.bend as E

# The last element is READ, not cleared: the invariant says nothing about the
# slots above the size, so clearing it would be one array write per pop that
# the algorithm does not need (the C reference does not do it either).
#
# The root slot of a nonempty heap is Some; the None case cannot be reached
# from a well-formed heap and returns the state unchanged.
def pop_with(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, mr: Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
  match mr:
    case None{}:
      (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})
    case Some{+root}:
      pop_last(~A, ~cmp, Nat.sub(size, 1n), U32.sub(n, 1), depth, cap, root, Array.get(Maybe<&2, A>, arr, U32.sub(n, 1)))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/containers/binary_heap.bend&name=Heap
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/containers/binary_heap.bend&name=pop_last
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/containers/types/binary_heap.bend&name=Error