ProofDigits.BK: def of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits
Lines 290-329 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=290&end_line=329

import Base

# A bound on n when put_dec.digits has fuel k: 10^(k+1) - 1, capped at the
# largest U32 from k = 9 on (all word constants, never a Nat above 2^32).
def BK(k: Nat) -> U32:
  match k:
    case 0n:
      9
    case 1n+a0:
      match a0:
        case 0n:
          99
        case 1n+a1:
          match a1:
            case 0n:
              999
            case 1n+a2:
              match a2:
                case 0n:
                  9999
                case 1n+a3:
                  match a3:
                    case 0n:
                      99999
                    case 1n+a4:
                      match a4:
                        case 0n:
                          999999
                        case 1n+a5:
                          match a5:
                            case 0n:
                              9999999
                            case 1n+a6:
                              match a6:
                                case 0n:
                                  99999999
                                case 1n+a7:
                                  match a7:
                                    case 0n:
                                      999999999
                                    case 1n+a8:
                                      U32.not(0)

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.not