law strided_length

mlbend-generative@0.1.1.0 · main.bend:308

import Base

308# LAW 5 (strided_length): every k-th entry of n entries is exactly the
309# number the count says.
310law strided_length:
311  for -A: Data
312  for +xs: List<&2, A>
313  for +k: Nat
314  for +skip: Nat
315  {List.length(&2, A, strided_from(A, xs, k, skip)) == groups_of(List.length(&2, A, xs), k, skip) : Nat}