original.name="Function_Valid_18"
======
>>> main.whiley
type nat is (int x) where x >= 0

function abs(int x) -> (nat r)
ensures r == x || r == -x
ensures r >= 0:
    //
    if x >= 0:
        return (nat) x
    else:
        return (nat) -x

function nop(nat item) -> (nat r)
ensures item == r:
    //
    return abs(item)

public export method test() :
    nat xs = abs(-123)
    assume xs == 123
    xs = nop(1)
    assume xs == 1

---