BendMlTensorArray.ASet.top_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 2316-2326 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=2316&end_line=2326

import Base

def 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}:
  match r:
    case Tuple{b, r1}:
      match r1:
        case Tuple{+n, r2}:
          match r2:
            case Tuple{+p, r3}:
              match r3:
                case Tuple{+q, r4}:
                  %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})
                  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)))

Uses (13):
  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.set
  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.Copy
  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.Z
  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.close_other
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.sz