law reshape_flat

bend-ml-tensor@0.1.2.0 · main.bend:489

import Base

489# LAW (reshape_flat): r x c has the same number of elements as 1 x (r*c)
490# (multiplying by 1 changes nothing), so flattening a matrix always exists.
491law reshape_flat:
492  for +r: Nat
493  for +c: Nat
494  {Nat.mul(r, c) == Nat.mul(1n, Nat.mul(r, c)) : Nat}