def bq.m

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:42

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U

42def bq.m(+lo: U32, +hi: U32) -> Nat:
43  Nat.add(U32.to_nat(lo), U.uq.half(Nat.sub(U32.to_nat(hi), U32.to_nat(lo))))