Decimal.Decimal.frac.go: def of bend-kit-bignum@0.1.0.0 Import: import bend-kit-bignum@0.1.0.0/decimal.bend as Decimal Lines 102-130 of bend-kit-bignum@0.1.0.0/decimal.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-bignum@0.1.0.0/decimal.bend&start_line=102&end_line=130 import Base import bend-kit-bignum@0.1.0.0/bigint.bend as Big # Each step divides d by 2 or 5 and scales n to match, so a d of D digits # needs fewer than 4D steps; f is that bound. def Decimal.frac.go(f: Nat, n: Big.BigInt, k: Nat, one: Bool, t2: Bool & Big.BigInt, t5: Bool & Big.BigInt) -> Maybe<&2, Decimal>: match f: case 0n: None{} case 1n+g: match one: case True{}: Some{Decimal{n, k}} case False{}: (z2, q2) = t2 match z2: case True{}: +d = {q2 : Big.BigInt} Decimal.frac.go(g, Big.BigInt.mul(n, Big.BigInt.from_u32(5)), 1n+k, Decimal.is_one(d), Decimal.divk(d, 2), Decimal.divk(d, 5)) case False{}: (z5, q5) = t5 match z5: case True{}: +d = {q5 : Big.BigInt} Decimal.frac.go(g, Big.BigInt.mul(n, Big.BigInt.from_u32(2)), 1n+k, Decimal.is_one(d), Decimal.divk(d, 2), Decimal.divk(d, 5)) case False{}: None{} Uses (11): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=bend-kit-bignum@0.1.0.0/bigint.bend&name=BigInt https://jend.leeeet.dev/definition.txt?path=bend-kit-bignum@0.1.0.0/bigint.bend&name=BigInt.from_u32 https://jend.leeeet.dev/definition.txt?path=bend-kit-bignum@0.1.0.0/bigint.bend&name=BigInt.mul https://jend.leeeet.dev/definition.txt?path=bend-kit-bignum@0.1.0.0/decimal.bend&name=Decimal https://jend.leeeet.dev/definition.txt?path=bend-kit-bignum@0.1.0.0/decimal.bend&name=Decimal.divk https://jend.leeeet.dev/definition.txt?path=bend-kit-bignum@0.1.0.0/decimal.bend&name=Decimal.is_one