def mid

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

import Base

171# Binary search for the last r in [lo, hi) where the test holds, given it
172# holds at lo and fails at hi (reference section 8.5 notes the float-sqrt
173# shortcut is wrong above 2^52; this search is exact). `more` is lo + 1 < hi
174# and `ok` is the test at the midpoint; the fuel bounds the halvings.
175def mid(+lo: Nat, +hi: Nat) -> Nat:
176  Nat.div(Nat.add(lo, hi), 2n)