def sort

ezx@1.11.0.0 · src/ez/sorted.bend:34

import Base

34# the strings in order. Base's List.sort takes its comparison as an erased
35# argument and is fuelled besides, so nothing downstream of it can be proved;
36# an insertion shrinks its list every step and stays inside the check.
37def sort(ss: List<&2, String>) -> List<&2, String>:
38  match ss:
39    case []:
40      []
41    case +h <> t:
42      sort.ins(h, sort(t))