def BitCount.value

bend-collections-laws-math@1.0.0.0 · spec/math/fixed.bend:184

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

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