foo.bend checks

raw source on the hub · import 0xab13df3d6c442b9408d79d186652b3aa/foo.bend as Foo

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)

1 import

import Base

Laws

law l123 provedsource · line 9 · raw

List<&2, U32>

law l321 provedsource · line 15 · raw

List<&2, U32>

law insert.put provedsource · line 21 · raw

@+x:U32 -> @h:U32 -> @+t:List<&2, U32> -> @r:List<&2, U32> -> @f:Bool -> List<&2, U32>

law insert provedsource · line 36 · raw

@+x:U32 -> @+xs:List<&2, U32> -> List<&2, U32>

law sort provedsource · line 48 · raw

@xs:List<&2, U32> -> List<&2, U32>

law rev provedsource · line 59 · raw

{List.reverse(&2, U32, l123) == l321 : List<&2, U32>}

law rev2 provedsource · line 65 · raw

{List.reverse(&2, U32, List.reverse(&2, U32, l123)) == l123 : List<&2, U32>}

law srt provedsource · line 71 · raw

{sort([3, 1, 2, 3]) == [1, 2, 3, 3] : List<&2, U32>}