def ASet.close_other
bend-ml-tensor-array@0.1.19.0 · main.bend:2290
import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base
2290def ASet.close_other(-T: Data, -b: Array<T>, +n: U32, +i: U32, +k: U32, +v: T, +q: {n == ASet.sz(T, b) : U32}, f: ASet.Both(T, b, n, ASet.J(i, n), v, ASet.Z(i, n), ASet.J(k, n), ASet.Z(k, n))) -> ASet.Apart(T, b, ASet.sz(T, b), ASet.J(i, ASet.sz(T, b)), ASet.Z(i, ASet.sz(T, b)), ASet.J(k, ASet.sz(T, b)), ASet.Z(k, ASet.sz(T, b))) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, b, i, v), k)) == Pair.snd(Array<T>, T, Array.get(T, b, k)) : T}:
2291 match f:
2292 case Tuple{o, r}:
2293 match o:
2294 case Tuple{+c1, o1}:
2295 match o1:
2296 case Tuple{+c2, o2}:
2297 match o2:
2298 case Tuple{+c3, o3}:
2299 match o3:
2300 case Tuple{+c4, o4}:
2301 match r:
2302 case Tuple{+d, r1}:
2303 match r1:
2304 case Tuple{+e1, r2}:
2305 match r2:
2306 case Tuple{+e2, r3}:
2307 match r3:
2308 case Tuple{e3, u}:
2309 %c1 : (ASet.Apart(T, b, ASet.sz(T, b), ASet.J(i, ASet.sz(T, b)), ASet.Z(i, ASet.sz(T, b)), ASet.J(k, ASet.sz(T, b)), ASet.Z(k, ASet.sz(T, b))) -> {Pair.snd(Array<T>, T, Array.get.at(T, k, Array.size(T, Array.set.fin(T, Array.swap.at(T, i, v, _))))) == Pair.snd(Array<T>, T, Array.get.at(T, k, _)) : T})
2310 %q : (ASet.Apart(T, b, _, ASet.J(i, _), ASet.Z(i, _), ASet.J(k, _), ASet.Z(k, _)) -> {Pair.snd(Array<T>, T, Array.get.at(T, k, Array.size(T, Array.set.fin(T, Array.swap.go(T, b, _, ASet.J(i, _), v, ASet.Z(i, _)))))) == Pair.snd(Array<T>, T, Array.get.go(T, b, _, ASet.J(k, _), ASet.Z(k, _))) : T})
2311 %c3 : (ASet.Apart(T, b, n, ASet.J(i, n), ASet.Z(i, n), ASet.J(k, n), ASet.Z(k, n)) -> {Pair.snd(Array<T>, T, Array.get.at(T, k, _)) == Pair.snd(Array<T>, T, Array.get.go(T, b, n, ASet.J(k, n), ASet.Z(k, n))) : T})
2312 %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)) : (ASet.Apart(T, b, n, ASet.J(i, n), ASet.Z(i, n), ASet.J(k, n), ASet.Z(k, n)) -> {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(k, _), ASet.Z(k, _))) == Pair.snd(Array<T>, T, Array.get.go(T, b, n, ASet.J(k, n), ASet.Z(k, n))) : T})
2313 e3