def search_go

bend-collections-laws-math@1.0.0.0 · src/math/natural.bend:198

import Base

198# the test is r^k <= n
199def search_go(fuel: Nat, +n: Nat, +k: Nat, +lo: Nat, +hi: Nat, +more: Bool, +ok: Bool) -> Nat:
200  match fuel more ok:
201    case 0n _ _:
202      lo
203    case 1n+f False{} _:
204      lo
205    case 1n+f True{} True{}:
206      search_go(f, n, k, mid(lo, hi), hi, Nat.is_lt(1n+mid(lo, hi), hi), root_le(n, k, mid(mid(lo, hi), hi)))
207    case 1n+f True{} False{}:
208      search_go(f, n, k, lo, mid(lo, hi), Nat.is_lt(1n+lo, mid(lo, hi)), root_le(n, k, mid(lo, mid(lo, hi))))