def bsearch.array.go

bend-osdev-algo@0.1.0.0 · bsearch.bend:112

import Base

112# fuel bounds the halvings: 33 is enough for any [lo, hi) of U32; once the
113# range is empty the remaining steps change nothing
114def bsearch.array.go(fuel: Nat, st: BsearchState, +key: U32) -> Array<U32> & U32:
115  match fuel:
116    case 0n:
117      bsearch.array.result(st)
118    case 1n+f:
119      bsearch.array.go(f, bsearch.array.advance(st, key), key)