law matrix_rows

mlbend-report@0.1.0.0 · main.bend:101

import Base

101# LAW 1 (matrix_rows): n rows of the matrix are n rows.
102law matrix_rows:
103  for +ys: List<&2, Nat>
104  for +ps: List<&2, Nat>
105  for +k: Nat
106  for +n: Nat
107  for +i: Nat
108  {rows_of(matrix_from(ys, ps, k, n, i)) == n : Nat}