law split_covers

mlbend-split@0.1.1.0 · main.bend:29

import Base

29# LAW (split_covers): every row of the dataset is placed in a fold — the
30# fold list holds one entry per row, so the folds are a partition of the
31# rows: the test rows of a fold and its training rows are disjoint, and
32# together they hold every row.
33law split_covers:
34  for labels: List<&2, Nat>
35  for +orders: List<&2, List<&2, Nat>>
36  for +k: Nat
37  for +i: Nat
38  {count_rows(folds_from(labels, orders, k, i)) == List.length(&2, Nat, labels) : Nat}