def MatT.sub_col

bend-tensors@0.0.0.2 · bend_tensors.bend:1025

import Base

1025# row i minus v_i: v is a VecT(r), one scalar per row
1026def MatT.sub_col(+r: Nat, +c: Nat, m: MatT(r, c), +v: VecT(r)) -> MatT(r, c):
1027  match r c:
1028    case 0n 0n:
1029      MatB{b} = m
1030      VecL{x} = v
1031      MatB{Blk.sub_col(b, x)}
1032    case 1n+p 0n:
1033      MatR{t, b} = m
1034      VecN{vt, vb} = v
1035      x y = MatT.sub_col(p, 0n, t, vt) MatT.sub_col(p, 0n, b, vb)
1036      MatR{x, y}
1037    case 0n 1n+q:
1038      MatC{l, r2} = m
1039      x y = MatT.sub_col(0n, q, l, v) MatT.sub_col(0n, q, r2, v)
1040      MatC{x, y}
1041    case 1n+p 1n+q:
1042      MatQ{a, b, c2, d} = m
1043      VecN{vt, vb} = v
1044      w x y z = MatT.sub_col(p, q, a, vt) MatT.sub_col(p, q, b, vt) MatT.sub_col(p, q, c2, vb) MatT.sub_col(p, q, d, vb)
1045      MatQ{w, x, y, z}