Bendtorch.pmul: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/main.bend as Bendtorch
Lines 2475-2482 of bendtorch@1.3.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/main.bend&start_line=2475&end_line=2482

import Base

# o[i·ow + oc + d] = a[i·t + 0]·b[0·bs + bc + d] + ... + a[i·t + t-1]·b[(t-1)·bs + bc + d], for idx = i·c + d from idx
# on, left more after r (P·V, and dQ = G·K): each sum left to right from +0.0
def pmul(left: Nat, +idx: U32, +c: U32, +t: Nat, +bs: U32, +bc: U32, +ow: U32, +oc: U32, o: Array<F32>, r: D2) -> PO:
  match left r:
    case 0n D2{a, b, +s}:
      PO{a, b, Array.set(F32, o, ((U32.div(idx, c) * ow : U32) + (oc + U32.mod(idx, c) : U32) : U32), s)}
    case 1n+n D2{a, b, +s}:
      pmul(n, (idx + 1 : U32), c, t, bs, bc, ow, oc, Array.set(F32, o, ((U32.div(idx, c) * ow : U32) + (oc + U32.mod(idx, c) : U32) : U32), s), dot0(t, (U32.div((idx + 1 : U32), c) * U32.from_nat(t) : U32), (bc + U32.mod((idx + 1 : U32), c) : U32), 1, bs, a, b))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=D2
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=PO
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=dot0