def bit_count_go

bend-collections-laws-math@1.0.0.0 · src/math/number.bend:25

import Base

25# n halves every step, so n steps are enough
26def bit_count_go(fuel: Nat, +n: Nat, +acc: Nat) -> Nat:
27  match fuel n:
28    case 0n _:
29      acc
30    case 1n+f 0n:
31      acc
32    case 1n+f 1n+ +np:
33      bit_count_go(f, Nat.div(1n+np, 2n), Nat.add(acc, Nat.mod(1n+np, 2n)))