def ub_row

bendtorch@1.3.0.0 · main.bend:2800

import Base

2800# one sequence's units (t x gw each) into o's rows r0.. at columns 0, gw, 2·gw, ...
2801def ub_row(left: Nat, +j: Nat, +t: Nat, +gw: Nat, +w: Nat, +r0: Nat, r: UO) -> UO:
2802  match left r:
2803    case 1n+n UO{Con{x, rest}, o}:
2804      ub_row(n, 1n+j, t, gw, w, r0, UO{rest, block_in(t, gw, w, r0, Nat.mul(j, gw), x, o)})
2805    case _ r:
2806      r