BendMlTensorArray.ASet.side_node: 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 2138-2159 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=2138&end_line=2159 import Base def ASet.side_node(-T: Data, -xs: Array, -ys: Array, +n: U32, +k: U32, +w: Bool, sx: ASet.Side(T, xs, U32.shr(n), k, U32.is_lt(k, U32.shr(U32.shr(n)))), sy: ASet.Side(T, ys, U32.shr(n), U32.sub(k, U32.shr(n)), U32.is_lt(U32.sub(k, U32.shr(n)), U32.shr(U32.shr(n))))) -> ASet.Side(T, ANode{xs, ys}, n, k, w): match w: case True{}: match sx: case Tuple{+s1, r1}: match r1: case Tuple{+g1, u1}: match sy: case Tuple{+s2, r2}: match r2: case Tuple{+g2, u2}: ({(%s1 : {(ANode{xs, ys}, Pair.snd(Array, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array & U32}; {==}) : {(ANode{xs, ys}, ASet.sz(T, ANode{xs, ys})) == Array.size(T, ANode{xs, ys}) : Array & U32}}, {(%g1 : {(Pair.fst(Array, T, Array.swap.lo(T, ys, _)), Pair.snd(Array, T, Array.swap.lo(T, ys, _))) == Array.swap.lo(T, ys, _) : Array & T}; {==}) : {(Pair.fst(Array, T, Array.get.go(T, ANode{xs, ys}, n, k, True{})), Pair.snd(Array, T, Array.get.go(T, ANode{xs, ys}, n, k, True{}))) == Array.get.go(T, ANode{xs, ys}, n, k, True{}) : Array & T}}, Unit{}) case False{}: match sx: case Tuple{+s1, r1}: match r1: case Tuple{+g1, u1}: match sy: case Tuple{+s2, r2}: match r2: case Tuple{+g2, u2}: ({(%s1 : {(ANode{xs, ys}, Pair.snd(Array, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array & U32}; {==}) : {(ANode{xs, ys}, ASet.sz(T, ANode{xs, ys})) == Array.size(T, ANode{xs, ys}) : Array & U32}}, {(%g2 : {(Pair.fst(Array, T, Array.swap.hi(T, xs, _)), Pair.snd(Array, T, Array.swap.hi(T, xs, _))) == Array.swap.hi(T, xs, _) : Array & T}; {==}) : {(Pair.fst(Array, T, Array.get.go(T, ANode{xs, ys}, n, k, False{})), Pair.snd(Array, T, Array.get.go(T, ANode{xs, ys}, n, k, False{}))) == Array.get.go(T, ANode{xs, ys}, n, k, False{}) : Array & T}}, Unit{}) Uses (18): 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.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=Array.swap.lo 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.Side https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.sz