def file.sort

ezx@1.11.0.0 · src/pkg/pkg.bend:571

import Base

571# a file list in path order. Insertion rather than Base's `List.sort`: that one
572# is a fuelled bottom-up merge sort, whose recursion Bend cannot check, so it
573# is reported as unsafe and every proof downstream of it inherits the report.
574# An insertion sort shrinks its list at every step, so Bend checks it, and a
575# package's file set is small enough that the cost is not felt.
576def file.sort(fs: List<&2, Item>) -> List<&2, Item>:
577  match fs:
578    case []:
579      []
580    case Con{+h, t}:
581      file.ins(file.sort(t), h)