ProofDigits.lgo: def of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits
Lines 252-260 of lawful-fields@0.1.1.0/proof_digits.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&start_line=252&end_line=260

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=DG