def pw

bend-collections-laws-math@1.0.0.0 · proofs/lib/word.bend:321

import Base

321# 2^k as an n-bit word
322def pw(+n: Nat, +k: Nat) -> Word(n):
323  match n k:
324    case 0n _:
325      WNil{}
326    case 1n+p 0n:
327      WCon{True{}, Word.zero(p)}
328    case 1n+p 1n+j:
329      WCon{False{}, pw(p, j)}