law band_len

bend-ml-tensor-array@0.1.19.0 · main.bend:1848

import Base

1848# LAW (band_len): the product of one band with `rows` rows gives exactly `rows` numbers.
1849# 0 rows give the empty list; 1 + p rows go through the gemm, and g_len counts what is read back.
1850law band_len:
1851  for -r: Nat
1852  for +c: Nat
1853  for +rows: Nat
1854  for x: Array<F32>
1855  for w: Array<F32>
1856  {bl_len(r, c, bv_gemm(r, c, rows, rows, x, w)) == rows : Nat}