js.compile.ignore=true ===== >>> main.whiley function setz(int[] items, int x) -> (int[] r) requires x >= 0 && x < |items| ensures |r| == |items| ensures all { i in 0..|items| | i == x || items[i] == r[i] } ensures r[x] == 0: return items[x:=0] public export method test(): int[] xs = [1,2,3] assert setz(xs,0) == [0,2,3] assert setz(xs,1) == [1,0,3] assert setz(xs,2) == [1,2,0] ---