law mat_numel

bendtorch@1.3.0.0 · LAWS.bend:303

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

303# LAW (mat_numel): a Tensor<[r, c]> holds the r·c numbers of a Mat<r, c>, so of_mat and to_mat reuse the array as it is.
304law mat_numel:
305  for +r: Nat
306  for +c: Nat
307  {TT.numel([r, c]) == Nat.mul(r, c) : Nat}