def un.odd_bd

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

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

1307def un.odd_bd(b: Bool, +v: Nat) -> {U.U32Nat.odd(Nat.add(U.U32Nat.bit(b), Nat.double(v))) == U.U32Nat.bit(b) : Nat}:
1308  match b:
1309    case True{}:
1310      un.odd_d1(v)
1311    case False{}:
1312      un.odd_d(v)