def lgo

lawful-fields@0.1.1.0 · proof_digits.bend:252

import Base

252# Nat.show.fin as a list: d is the digit just produced, q what is left.
253def lgo(f: Nat, +q: Nat, +d: U32, acc: List<&2, U32>) -> List<&2, U32>:
254  match f q:
255    case _ 0n:
256      d <> acc
257    case 0n 1n+p:
258      d <> acc
259    case 1n+g 1n+p:
260      lgo(g, Nat.div(1n+p, 10n), DG(1n+p), d <> acc)