def pow_le_go

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

import Base

178# r^k <= n without forming a product above n: `ok` is acc * r <= n, asked
179# as acc <= n / r, and acc * r is only formed once it is known to fit.
180def pow_le_go(k: Nat, +r: Nat, +acc: Nat, +n: Nat, +ok: Bool) -> Bool:
181  match k ok:
182    case 0n _:
183      True{}
184    case 1n+j False{}:
185      False{}
186    case 1n+j True{}:
187      pow_le_go(j, r, Nat.mul(acc, r), n, Nat.is_le(Nat.mul(acc, r), Nat.div(n, r)))