def bq.x

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

import Base
import bend-osdev-array@0.1.0.0/array.bend as A

27# the element the search reads between lo and hi
28def bq.x(+d: Nat, +l: List<&2, U32>, +lo: U32, +hi: U32) -> U32:
29  A.Arrays.nth(U32, l, A.Arrays.index(d, bq.mid(lo, hi)), 0)