law one_hot_count_length

mlbend-preprocess@0.1.0.0 · main.bend:29

import Base

29# LAW (one_hot_count_length): the one-hot matrix has one row for every
30# label.
31law one_hot_count_length:
32  for ys: List<&2, Nat>
33  {one_hot_count_of(ys) == List.length(&2, Nat, ys) : Nat}