def ASet.top_other

bend-ml-tensor-array@0.1.19.0 · main.bend:2316

import Base

2316def ASet.top_other(-T: Data, -a: Array<T>, +i: U32, +k: U32, +v: T, r: ASet.Copy(T, a)) -> ASet.Apart(T, a, ASet.sz(T, a), ASet.J(i, ASet.sz(T, a)), ASet.Z(i, ASet.sz(T, a)), ASet.J(k, ASet.sz(T, a)), ASet.Z(k, ASet.sz(T, a))) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), k)) == Pair.snd(Array<T>, T, Array.get(T, a, k)) : T}:
2317  match r:
2318    case Tuple{b, r1}:
2319      match r1:
2320        case Tuple{+n, r2}:
2321          match r2:
2322            case Tuple{+p, r3}:
2323              match r3:
2324                case Tuple{+q, r4}:
2325                  %p : (ASet.Apart(T, _, ASet.sz(T, _), ASet.J(i, ASet.sz(T, _)), ASet.Z(i, ASet.sz(T, _)), ASet.J(k, ASet.sz(T, _)), ASet.Z(k, ASet.sz(T, _))) -> {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, _, i, v), k)) == Pair.snd(Array<T>, T, Array.get(T, _, k)) : T})
2326                  ASet.close_other(T, b, n, i, k, v, q, ASet.both(T, b, n, ASet.J(i, n), v, ASet.Z(i, n), ASet.J(k, n), ASet.Z(k, n)))