BendMlTensorArray.ASet.close_other: def of bend-ml-tensor-array@0.1.19.0
Import: import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
Lines 2290-2313 of bend-ml-tensor-array@0.1.19.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&start_line=2290&end_line=2313

import Base

def 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}:
  match f:
    case Tuple{o, r}:
      match o:
        case Tuple{+c1, o1}:
          match o1:
            case Tuple{+c2, o2}:
              match o2:
                case Tuple{+c3, o3}:
                  match o3:
                    case Tuple{+c4, o4}:
                      match r:
                        case Tuple{+d, r1}:
                          match r1:
                            case Tuple{+e1, r2}:
                              match r2:
                                case Tuple{+e2, r3}:
                                  match r3:
                                    case Tuple{e3, u}:
                                      %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})
                                      %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})
                                      %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})
                                      %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})
                                      e3

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get.at
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.size
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.at
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.Apart
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.Both
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.J
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.NA
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.Z
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.sz