def w8

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as Fixbytes

import Base

232def w8(k: Nat) -> Nat:
233  match k:
234    case 0n:
235      0n
236    case 1n+p:
237      Nat.add(8n, w8(p))

Uses (2)