def un.wc

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

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

1122def un.wc(-p: Nat, b: Bool, -t: Word(p)) -> {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(U.U32Nat.bit(b), Nat.double(Word.to_nat(p, t))) : Nat}:
1123  match b:
1124    case True{}:
1125      {==}
1126    case False{}:
1127      {==}