Fixed.BitCount.value: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as Fixed
Lines 184-185 of bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend&start_line=184&end_line=185

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN

def BitCount.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> Nat, +w: Nat, +a: T) -> Type:
  {f(a) == SN.ones(w, val(a)) : Nat}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=ones