def half_bit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbits.bend:32

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

32def half_bit(+n: Nat) -> {C.half(C.bit(n)) == 0n : Nat}:
33  match n:
34    case 0n:
35      {==}
36    case 1n:
37      {==}
38    case 2n+ +q:
39      half_bit(q)