def un.bv

bend-osdev-u32@0.1.0.0 · PROOF.bend:331

import Base

331def un.bv(b: Bool, x: Nat) -> Nat:
332  match b:
333    case False{}:
334      Nat.double(x)
335    case True{}:
336      1n+Nat.double(x)