def BK

lawful-fields@0.1.1.0 · proof_digits.bend:290

import Base

290# A bound on n when put_dec.digits has fuel k: 10^(k+1) - 1, capped at the
291# largest U32 from k = 9 on (all word constants, never a Nat above 2^32).
292def BK(k: Nat) -> U32:
293  match k:
294    case 0n:
295      9
296    case 1n+a0:
297      match a0:
298        case 0n:
299          99
300        case 1n+a1:
301          match a1:
302            case 0n:
303              999
304            case 1n+a2:
305              match a2:
306                case 0n:
307                  9999
308                case 1n+a3:
309                  match a3:
310                    case 0n:
311                      99999
312                    case 1n+a4:
313                      match a4:
314                        case 0n:
315                          999999
316                        case 1n+a5:
317                          match a5:
318                            case 0n:
319                              9999999
320                            case 1n+a6:
321                              match a6:
322                                case 0n:
323                                  99999999
324                                case 1n+a7:
325                                  match a7:
326                                    case 0n:
327                                      999999999
328                                    case 1n+a8:
329                                      U32.not(0)