foo.bend source

foo.bend on the hub · documented module

# base List: reverse is involutive and an insertion sort orders (dupes# kept) on concrete lists -- closed by conversion alone, no output.# ported from bend3: list literals become Con/Nil spines, bend3-base# List.sort becomes a local insertion sort (bend base has none); the# compare-and-rebuild double use takes + binders (List<&2, U32> is# Data, so it duplicates)import Baselaw l123:  List<&2, U32>def l123():  [1, 2, 3]law l321:  List<&2, U32>def l321():  [3, 2, 1]law insert.put:  for +x: U32  for  h: U32  for +t: List<&2, U32>  for  r: List<&2, U32>  for  f: Bool  List<&2, U32>def insert.put(x, h, t, r, f):  match f:    case True{}:      x <> h <> t    case False{}:      h <> rlaw insert:  for +x  : U32  for +xs : List<&2, U32>  List<&2, U32>def insert(x, xs):  match xs:    case Nil{}:      [x]    case h <> t:      insert.put(x, h, t, insert(x, t), U32.is_le(x, h))law sort:  for xs: List<&2, U32>  List<&2, U32>def sort(xs):  match xs:    case Nil{}:      Nil{}    case h <> t:      insert(h, sort(t))law rev:  {List.reverse(&2, U32, l123) == l321 : List<&2, U32>}def rev():  {==}law rev2:  {List.reverse(&2, U32, List.reverse(&2, U32, l123)) == l123 : List<&2, U32>}def rev2():  {==}law srt:  {sort([3, 1, 2, 3]) == [1, 2, 3, 3] : List<&2, U32>}def srt():  {==}#|All terms check.