BendMlTensorArray.ASet.reads_t: 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 2194-2224 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=2194&end_line=2224 import Base # the write goes into the low half xs def ASet.reads_t(-T: Data, -xs: Array, -ys: Array, +n: U32, +j: U32, +v: T, +k: U32, +w: Bool, +g: {(Pair.fst(Array, T, ASet.RH(T, ys, n, k)), Pair.snd(Array, T, ASet.RH(T, ys, n, k))) == ASet.RH(T, ys, n, k) : Array & T}, r: ASet.Reads(T, xs, U32.shr(n), j, v, U32.is_lt(j, U32.shr(U32.shr(n))), k, U32.is_lt(k, U32.shr(U32.shr(n))))) -> ASet.Reads(T, ANode{xs, ys}, n, j, v, True{}, k, w): match w: case True{}: match r: case Tuple{+d, r1}: match r1: case Tuple{+e1, r2}: match r2: case Tuple{+e2, r3}: match r3: case Tuple{e3, u}: ({(%d : {(Array.set.fin(T, Array.swap.lo(T, ys, _)), Pair.snd(Array, T, Array.swap.lo(T, ys, _))) == Array.swap.lo(T, ys, _) : Array & T}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), Pair.snd(Array, T, ASet.G(T, ANode{xs, ys}, n, j, v, True{}))) == ASet.G(T, ANode{xs, ys}, n, j, v, True{}) : Array & T}}, {(%e1 : {(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}}, {(%d : {(Pair.fst(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, True{})), Pair.snd(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, True{}))) == Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, True{}) : Array & T}; %e2 : {(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, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), n, k, True{})), Pair.snd(Array, T, Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), n, k, True{}))) == Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), n, k, True{}) : Array & T}}, (h => (%d : {Pair.snd(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, True{})) == Pair.snd(Array, T, Array.get.go(T, ANode{xs, ys}, n, k, True{})) : T}; %e2 : {Pair.snd(Array, T, Array.swap.lo(T, ys, _)) == Pair.snd(Array, T, Array.swap.lo(T, ys, ASet.RL(T, xs, n, k))) : T}; %e1 : {Pair.snd(Array, T, ASet.RL(T, ASet.WL(T, xs, n, j, v), n, k)) == Pair.snd(Array, T, Array.swap.lo(T, ys, _)) : T}; e3(h))), Unit{}) case False{}: match r: case Tuple{+d, r1}: match r1: case Tuple{+e1, r2}: match r2: case Tuple{+e2, r3}: match r3: case Tuple{e3, u}: ({(%d : {(Array.set.fin(T, Array.swap.lo(T, ys, _)), Pair.snd(Array, T, Array.swap.lo(T, ys, _))) == Array.swap.lo(T, ys, _) : Array & T}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), Pair.snd(Array, T, ASet.G(T, ANode{xs, ys}, n, j, v, True{}))) == ASet.G(T, ANode{xs, ys}, n, j, v, True{}) : Array & T}}, {(%g : {(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}}, {(%d : {(Pair.fst(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, False{})), Pair.snd(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, False{}))) == Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, False{}) : Array & T}; %g : {(Pair.fst(Array, T, Array.swap.hi(T, ASet.WL(T, xs, n, j, v), _)), Pair.snd(Array, T, Array.swap.hi(T, ASet.WL(T, xs, n, j, v), _))) == Array.swap.hi(T, ASet.WL(T, xs, n, j, v), _) : Array & T}; {==}) : {(Pair.fst(Array, T, Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), n, k, False{})), Pair.snd(Array, T, Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), n, k, False{}))) == Array.get.go(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), n, k, False{}) : Array & T}}, (h => (%d : {Pair.snd(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, k, False{})) == Pair.snd(Array, T, Array.get.go(T, ANode{xs, ys}, n, k, False{})) : T}; %g : {Pair.snd(Array, T, Array.swap.hi(T, ASet.WL(T, xs, n, j, v), _)) == Pair.snd(Array, T, Array.swap.hi(T, xs, _)) : T}; {==})), Unit{}) 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.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.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=Unit 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.NA https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.RH https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.RL https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.Reads https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=ASet.WL