def ASet.close_get
bend-ml-tensor-array@0.1.19.0 · main.bend:2054
import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base
2054def ASet.close_get(-T: Data, -b: Array<T>, +n: U32, +i: U32, +v: T, +q: {n == ASet.sz(T, b) : U32}, f: ASet.Facts(T, b, n, ASet.J(i, n), v, ASet.Z(i, n))) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, b, i, v), i)) == v : T}:
2055 match f:
2056 case Tuple{+c1, r1}:
2057 match r1:
2058 case Tuple{+c2, r2}:
2059 match r2:
2060 case Tuple{+c3, r3}:
2061 match r3:
2062 case Tuple{+c4, r4}:
2063 match r4:
2064 case Tuple{+c5, r5}:
2065 %c1 : {Pair.snd(Array<T>, T, Array.get.at(T, i, Array.size(T, Array.set.fin(T, Array.swap.at(T, i, v, _))))) == v : T}
2066 %q : {Pair.snd(Array<T>, T, Array.get.at(T, i, Array.size(T, Array.set.fin(T, Array.swap.go(T, b, _, ASet.J(i, _), v, ASet.Z(i, _)))))) == v : T}
2067 %c3 : {Pair.snd(Array<T>, T, Array.get.at(T, i, _)) == v : T}
2068 %Equal.trans(U32, n, ASet.sz(T, b), ASet.sz(T, ASet.NA(T, b, n, ASet.J(i, n), v, ASet.Z(i, n))), q, Equal.sym(U32, ASet.sz(T, ASet.NA(T, b, n, ASet.J(i, n), v, ASet.Z(i, n))), ASet.sz(T, b), c4)) : {Pair.snd(Array<T>, T, Array.get.go(T, ASet.NA(T, b, n, ASet.J(i, n), v, ASet.Z(i, n)), _, ASet.J(i, _), ASet.Z(i, _))) == v : T}
2069 c5