whiley_test_file 0.6.2

original.name="EffectiveList_Valid_1"
======
>>> main.whiley
type rec is {int y, int x}
type nbool is bool|null

function f(int[] xs) -> nbool[]:
    nbool[] r = [false; |xs|]
    int i = 0
    while i < |xs|
        where i >= 0
        where |xs| == |r|:
        //
        if xs[i] < 0:
            r[i] = true
        else:
            r[i] = null
        i = i + 1
    return r

public export method test() :
    int[] e = [0;0]
    assume f(e) == []
    e = [1, 2, 3, 4]
    assume f(e) == [null,null,null,null]

---