BendTensors.MatT.sum_rows: def of bend-tensors@0.0.0.2 Import: import bend-tensors@0.0.0.2/bend_tensors.bend as BendTensors Lines 942-959 of bend-tensors@0.0.0.2/bend_tensors.bend: https://jend.leeeet.dev/read.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&start_line=942&end_line=959 import Base # each row's sum: VecT(r) def MatT.sum_rows(+r: Nat, +c: Nat, m: MatT(r, c)) -> VecT(r): match r c: case 0n 0n: MatB{b} = m VecL{Blk.sum_rows(b)} case 1n+p 0n: MatR{t, b} = m x y = MatT.sum_rows(p, 0n, t) MatT.sum_rows(p, 0n, b) VecN{x, y} case 0n 1n+q: MatC{l, r2} = m x y = MatT.sum_rows(0n, q, l) MatT.sum_rows(0n, q, r2) VecT.add(0n, x, y) case 1n+p 1n+q: MatQ{a, b, c2, d} = m p0 q0 p1 q1 = MatT.sum_rows(p, q, a) MatT.sum_rows(p, q, b) MatT.sum_rows(p, q, c2) MatT.sum_rows(p, q, d) VecT.add2(p, p0, q0, p1, q1) Uses (12): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=Blk.sum_rows https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=MatT https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=MatT.Cols https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=MatT.Leaf https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=MatT.Quad https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=MatT.Rows https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=VecT https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=VecT.Leaf https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=VecT.Node https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=VecT.add https://jend.leeeet.dev/definition.txt?path=bend-tensors@0.0.0.2/bend_tensors.bend&name=VecT.add2