original.name="Function_Valid_29"
======
>>> main.whiley
function get(int[] xs, int i) -> (int r)
requires 0 <= i && i < |xs|
ensures r == xs[i]:
return xs[i]
public export method test():
int i = 0
int[] xs = [1,2,3,0,2]
//
if i < |xs| && get(xs,i) != 0:
i = i + 1
//
assert i == 1
---