whiley_test_file 0.6.2

original.name="ConstrainedList_Valid_14"
======
>>> main.whiley


type wierd is (int[] xs) where some { i in 0..|xs| | xs[i] > 0 }

function f(int[] xs) -> wierd
requires |xs| > 0:
    xs[0] = 1
    assert xs is wierd
    return xs

public export method test() :
    assume f([-1, -2]) == [1,-2]

---