law to_list_len

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

import Base

1884# LAW (to_list_len): Mat.to_list reads exactly r*c numbers, no more and no fewer.
1885law to_list_len:
1886  for +r: Nat
1887  for +c: Nat
1888  for m: Mat<r, c>
1889  {ML.len(r, c, Mat.to_list(r, c, m)) == Nat.mul(r, c) : Nat}