Natural.ilog_ok: def of bend-collections@1.0.0.0 Import: import bend-collections@1.0.0.0/src/math/natural.bend as Natural Lines 263-268 of bend-collections@1.0.0.0/src/math/natural.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/math/natural.bend&start_line=263&end_line=268 import Base def ilog_ok(+n: Nat, +b: Nat, +bad: Bool) -> Result<&2, &2, MathError, Nat>: match bad: case True{}: Fail{Domain{}} case False{}: Done{ilog_go(n, n, b, 0n, 1n, Nat.is_le(1n, Nat.div(n, b)))} Uses (7): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/math/natural.bend&name=MathError https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/math/natural.bend&name=ilog_go