law select_covers

mlbend-select@0.1.0.0 · main.bend:25

import Base
import mlbend-split@0.1.1.0/main.bend as Split

25# LAW (select_covers): every row of the dataset is in exactly one fold —
26# the fold list holds one entry per row, so the folds cover the dataset
27# exactly once each.
28law select_covers:
29  for labels: List<&2, Nat>
30  for +orders: List<&2, List<&2, Nat>>
31  for +k: Nat
32  for +i: Nat
33  {Split.count_rows(Split.folds_from(labels, orders, k, i)) == List.length(&2, Nat, labels) : Nat}