def MatT.add_row

bend-tensors@0.0.0.2 · bend_tensors.bend:1003

import Base

1003# v added to every row: v is a VecT(c)
1004def MatT.add_row(+r: Nat, +c: Nat, m: MatT(r, c), +v: VecT(c)) -> MatT(r, c):
1005  match r c:
1006    case 0n 0n:
1007      MatB{b} = m
1008      VecL{x} = v
1009      MatB{Blk.add_row(b, x)}
1010    case 1n+p 0n:
1011      MatR{t, b} = m
1012      x y = MatT.add_row(p, 0n, t, v) MatT.add_row(p, 0n, b, v)
1013      MatR{x, y}
1014    case 0n 1n+q:
1015      MatC{l, r2} = m
1016      VecN{vl, vr} = v
1017      x y = MatT.add_row(0n, q, l, vl) MatT.add_row(0n, q, r2, vr)
1018      MatC{x, y}
1019    case 1n+p 1n+q:
1020      MatQ{a, b, c2, d} = m
1021      VecN{vl, vr} = v
1022      w x y z = MatT.add_row(p, q, a, vl) MatT.add_row(p, q, b, vr) MatT.add_row(p, q, c2, vl) MatT.add_row(p, q, d, vr)
1023      MatQ{w, x, y, z}