law count_length

mlbend-metrics@0.1.0.0 · main.bend:96

import Base

96# LAW 1 (count_length): the number of samples is the length of the list
97# of labels. (The count is this package's own walk, so the law pins it
98# to the length Base counts.)
99law count_length:
100  for ys: List<&2, Nat>
101  {count(ys) == List.length(&2, Nat, ys) : Nat}