~/bend-docscommunity

proofs/math/number/bitcount.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend as Bitcount

7 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/number.bend as NB
import ../../../spec/math/number.bend as SN
import ../typed/width.bend as WW

Definitions

def half_div2 source · line 13 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n) == Nat.div(n, 2n) : Nat}

def ones_zero source · line 22 · raw

@+k:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(k, 0n) == 0n : Nat}

def go source · line 30 · raw

@+f:Nat -> @+n:Nat -> @+acc:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.bit_count_go(f, n, acc) == Nat.add(acc, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.ones(f, n)) : Nat}

the loop adds the ones of its fuel's worth of bits

def bit_count_value source · line 43 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.BitCount.value(n)