Lock.pack.sort: def of ezx@1.11.0.0
Import: import ezx@1.11.0.0/src/lock/lock.bend as Lock
Lines 495-505 of ezx@1.11.0.0/src/lock/lock.bend: https://jend.leeeet.dev/read.txt?path=ezx@1.11.0.0/src/lock/lock.bend&start_line=495&end_line=505

import Base

# the packages in hash order. Insertion rather than Base's `List.sort`: that
# one is a fuelled bottom-up merge sort, whose recursion Bend cannot check, so
# it is reported as unsafe and every proof downstream of it inherits the
# report. An insertion sort shrinks its list at every step, so Bend checks it,
# and a lock names tens of packages, not thousands.
def pack.sort(ps: List<&2, Pack>) -> List<&2, Pack>:
  match ps:
    case []:
      []
    case Con{+h, t}:
      pack.ins(pack.sort(t), h)

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=ezx@1.11.0.0/src/lock/lock.bend&name=Pack
  https://jend.leeeet.dev/definition.txt?path=ezx@1.11.0.0/src/lock/lock.bend&name=pack.ins