MlbendMetrics.count_length: law of mlbend-metrics@0.1.0.0
Import: import mlbend-metrics@0.1.0.0/main.bend as MlbendMetrics
Lines 96-101 of mlbend-metrics@0.1.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=mlbend-metrics@0.1.0.0/main.bend&start_line=96&end_line=101

import Base

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

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=mlbend-metrics@0.1.0.0/main.bend&name=count