def ones
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as Numberimport Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
20# the 1 bits among the k lowest bits of n
21def ones(k: Nat, +n: Nat) -> Nat:
22 match k:
23 case 0n:
24 0n
25 case 1n+p:
26 Nat.add(C.bit(n), ones(p, C.half(n)))
Uses (4)
Used by (10)
- bend-collections-laws-math@1.0.0.0/spec/math/fixed:BitCount.value
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits:bc_go
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits:ones_add
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits:ones_low
- bend-collections-laws-math@1.0.0.0/spec/math/number:BitCount.value
- …