def uq.bv

bend-osdev-algo@0.1.0.0 · proof_u32.bend:29

import Base

29# the value of a word's lowest bit and the rest
30def uq.bv(b: Bool, x: Nat) -> Nat:
31  match b:
32    case False{}:
33      Nat.double(x)
34    case True{}:
35      1n+Nat.double(x)