BendMlTensorArray.ASet.node_f: 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 1981-1994 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=1981&end_line=1994

import Base

def ASet.node_f(-T: Data, -xs: Array<T>, -ys: Array<T>, +n: U32, +j: U32, +v: T, +s: {(xs, ASet.sz(T, xs)) == Array.size(T, xs) : Array<T> & U32}, f: ASet.Facts(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n))))) -> ASet.Facts(T, ANode{xs, ys}, n, j, v, False{}):
  match f:
    case Tuple{+c1, r1}:
      match r1:
        case Tuple{+c2, r2}:
          match r2:
            case Tuple{+c3, r3}:
              match r3:
                case Tuple{+c4, r4}:
                  match r4:
                    case Tuple{+c5, r5}:
                      match r5:
                        case Tuple{+c6, u}:
                          ({(%s : {(ANode{xs, ys}, Pair.snd(Array<T>, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array<T> & U32}; {==}) : {(ANode{xs, ys}, ASet.sz(T, ANode{xs, ys})) == Array.size(T, ANode{xs, ys}) : Array<T> & U32}}, {(%c2 : {(Array.set.fin(T, Array.swap.hi(T, xs, _)), Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _))) == Array.swap.hi(T, xs, _) : Array<T> & T}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), Pair.snd(Array<T>, T, ASet.G(T, ANode{xs, ys}, n, j, v, False{}))) == ASet.G(T, ANode{xs, ys}, n, j, v, False{}) : Array<T> & T}}, {(%c2 : {(Array.set.fin(T, Array.swap.hi(T, xs, _)), ASet.sz(T, Array.set.fin(T, Array.swap.hi(T, xs, _)))) == Array.size(T, Array.set.fin(T, Array.swap.hi(T, xs, _))) : Array<T> & U32}; %s : {(ANode{xs, Array.set.fin(T, ASet.G(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n)))))}, Pair.snd(Array<T>, U32, Array.size.node(T, Array.set.fin(T, ASet.G(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n))))), _))) == Array.size.node(T, Array.set.fin(T, ASet.G(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n))))), _) : Array<T> & U32}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, False{}), ASet.sz(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{}))) == Array.size(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{})) : Array<T> & U32}}, {(%c2 : {ASet.sz(T, Array.set.fin(T, Array.swap.hi(T, xs, _))) == ASet.sz(T, ANode{xs, ys}) : U32}; %s : {Pair.snd(Array<T>, U32, Array.size.node(T, Array.set.fin(T, ASet.G(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), v, U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n))))), _)) == Pair.snd(Array<T>, U32, Array.size.node(T, ys, _)) : U32}; {==}) : {ASet.sz(T, ASet.NA(T, ANode{xs, ys}, n, j, v, False{})) == ASet.sz(T, ANode{xs, ys}) : U32}}, {(%c2 : {Pair.snd(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, j, False{})) == v : T}; %c6 : {Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _)) == v : T}; c5) : {Pair.snd(Array<T>, T, ASet.K(T, ANode{xs, ys}, n, j, v, False{})) == v : T}}, {(%c2 : {(Pair.fst(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, j, False{})), Pair.snd(Array<T>, T, Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, j, False{}))) == Array.get.go(T, Array.set.fin(T, Array.swap.hi(T, xs, _)), n, j, False{}) : Array<T> & T}; %c6 : {(Pair.fst(Array<T>, T, Array.swap.hi(T, xs, _)), Pair.snd(Array<T>, T, Array.swap.hi(T, xs, _))) == Array.swap.hi(T, xs, _) : Array<T> & T}; {==}) : {(Pair.fst(Array<T>, T, ASet.K(T, ANode{xs, ys}, n, j, v, False{})), Pair.snd(Array<T>, T, ASet.K(T, ANode{xs, ys}, n, j, v, False{}))) == ASet.K(T, ANode{xs, ys}, n, j, v, False{}) : Array<T> & T}}, Unit{})

Uses (21):
  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.go
  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.size.node
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.hi
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  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=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.Facts
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.G
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.K
  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.sz