law row_length

mlbend-report@0.1.0.0 · main.bend:120

import Base

120# LAW 2 (row_length): n cells of a row are n cells.
121law row_length:
122  for +ys: List<&2, Nat>
123  for +ps: List<&2, Nat>
124  for +k: Nat
125  for +i: Nat
126  for +n: Nat
127  for +j: Nat
128  {cells_of(row_from(ys, ps, k, i, n, j)) == n : Nat}