original.name="TypeEquals_Valid_59"
whiley.compile.ignore=true
WhileyCompiler.issue=1003
======
>>> main.whiley
type nat is (int n) where n >= 0

function f(int|int[]|(int|null)[] x) -> (int r)
ensures (x is int[] && |x| > 0) ==> (r == x[0]):
    //
    if x is int[] && |x| > 0:
        return x[0]
    else:
        return 0

public export method test():
    //
    (int|null)[] a1 = [123]
    (int|null)[] a2 = [null]
    int[] a3 = [124]
    //
    assert f(a1) == 123
    assert f(a2) == 0
    assert f(a3) == 124
    assert f(0) == 0
    //
---