def ilog_ok

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

import Base

263def ilog_ok(+n: Nat, +b: Nat, +bad: Bool) -> Result<&2, &2, MathError, Nat>:
264  match bad:
265    case True{}:
266      Fail{Domain{}}
267    case False{}:
268      Done{ilog_go(n, n, b, 0n, 1n, Nat.is_le(1n, Nat.div(n, b)))}