def pack.sort

ezx@1.11.0.0 · src/lock/lock.bend:495

import Base

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