def pow2u

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:153

import Base

153# 2^d as the U32 built by Base Array.size (1, then shl per level).
154def pow2u(d: Nat) -> U32:
155  match d:
156    case 0n:
157      1
158    case 1n+p:
159      U32.shl(pow2u(p))