def wd.bv

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:113

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

113def wd.bv(g: Bool) -> {U32.to_nat(W.W64.bit(g)) == U.U32Nat.bit(g) : Nat}:
114  match g:
115    case True{}:
116      {==}
117    case False{}:
118      {==}