def AP.nth_get

bend-osdev-array@0.1.0.1 · PROOF.bend:1471

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1471def AP.nth_get(-T: Data, -xs: List<&2, T>, -k: Nat, -f: T, -g: T, e: {List.get(&2, T, xs, k) == Some{g} : Maybe<&2, T>}) -> {A.Arrays.nth(T, xs, k, f) == g : T}:
1472  %Equal.sym(Maybe<&2, T>, List.get(&2, T, xs, k), Some{g}, e) : {A.Arrays.nth.or(T, _, f) == g : T}
1473  {==}