def wd.bl

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

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

120def wd.bl(g: Bool) -> {Nat.is_lt(U32.to_nat(W.W64.bit(g)), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}:
121  match g:
122    case True{}:
123      {==}
124    case False{}:
125      {==}