BendMlTensorArray.ASet.node_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 1966-1979 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=1966&end_line=1979 import Base def ASet.node_t(-T: Data, -xs: Array, -ys: Array, +n: U32, +j: U32, +v: T, f: ASet.Facts(T, xs, U32.shr(n), j, v, U32.is_lt(j, U32.shr(U32.shr(n))))) -> ASet.Facts(T, ANode{xs, ys}, n, j, v, True{}): 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}: ({(%c1 : {(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}}, {(%c2 : {(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}}, {(%c2 : {(Array.set.fin(T, Array.swap.lo(T, ys, _)), ASet.sz(T, Array.set.fin(T, Array.swap.lo(T, ys, _)))) == Array.size(T, Array.set.fin(T, Array.swap.lo(T, ys, _))) : Array & U32}; %c3 : {(ANode{Array.set.fin(T, ASet.G(T, xs, U32.shr(n), j, v, U32.is_lt(j, U32.shr(U32.shr(n))))), ys}, Pair.snd(Array, U32, Array.size.node(T, ys, _))) == Array.size.node(T, ys, _) : Array & U32}; {==}) : {(ASet.NA(T, ANode{xs, ys}, n, j, v, True{}), ASet.sz(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{}))) == Array.size(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{})) : Array & U32}}, {(%c2 : {ASet.sz(T, Array.set.fin(T, Array.swap.lo(T, ys, _))) == ASet.sz(T, ANode{xs, ys}) : U32}; %c3 : {Pair.snd(Array, U32, Array.size.node(T, ys, _)) == ASet.sz(T, ANode{xs, ys}) : U32}; %c1 : {U32.shl(ASet.sz(T, Array.set.fin(T, ASet.G(T, xs, U32.shr(n), j, v, U32.is_lt(j, U32.shr(U32.shr(n))))))) == Pair.snd(Array, U32, Array.size.node(T, ys, _)) : U32}; %c4 : {U32.shl(ASet.sz(T, Array.set.fin(T, ASet.G(T, xs, U32.shr(n), j, v, U32.is_lt(j, U32.shr(U32.shr(n))))))) == U32.shl(_) : U32}; {==}) : {ASet.sz(T, ASet.NA(T, ANode{xs, ys}, n, j, v, True{})) == ASet.sz(T, ANode{xs, ys}) : U32}}, {(%c2 : {Pair.snd(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, j, True{})) == v : T}; %c6 : {Pair.snd(Array, T, Array.swap.lo(T, ys, _)) == v : T}; c5) : {Pair.snd(Array, T, ASet.K(T, ANode{xs, ys}, n, j, v, True{})) == v : T}}, {(%c2 : {(Pair.fst(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, j, True{})), Pair.snd(Array, T, Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, j, True{}))) == Array.get.go(T, Array.set.fin(T, Array.swap.lo(T, ys, _)), n, j, True{}) : Array & T}; %c6 : {(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, ASet.K(T, ANode{xs, ys}, n, j, v, True{})), Pair.snd(Array, T, ASet.K(T, ANode{xs, ys}, n, j, v, True{}))) == ASet.K(T, ANode{xs, ys}, n, j, v, True{}) : Array & 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.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.shl 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.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