def BitCount.value

bend-collections-laws-math@1.0.0.0 · spec/math/number.bend:28

import Base
import bend-collections-laws-math@1.0.0.0/src/math/number.bend as NB

28# every n is below 2^n, so ones(n, n) counts all of n's 1 bits
29def BitCount.value(+n: Nat) -> Type:
30  {NB.bit_count(n) == ones(n, n) : Nat}