The decimal digits of a natural, most significant first ("0" for zero):
the text form of a counter, a sequence number or a tick in an AOS-JSON/1
stream (Observe.Value), and of a token cache path's ranges
(Data.TokenCachePath). `fuel` is the caller's bound on the number of
digits LESS ONE: a natural with more than `fuel + 1` digits keeps only its
last `fuel + 1`, so every caller names a bound its values cannot exceed
(a u64 has at most 20 digits).
302def naturalDecimalBuilder =
303 (lambda unrestricted fuel : Nat .
304 (nat-eliminate
305 (lambda unrestricted current : Nat . (pi unrestricted value : Nat . BytesBuilder))
306 (lambda unrestricted value : Nat .
307 (bytes-builder-chunk (bytes (nat-to-byte (naturalAdd 48 (naturalModuloUnchecked value 10))))))
308 (lambda unrestricted predecessor : Nat .
309 (lambda unrestricted induction : (pi unrestricted value : Nat . BytesBuilder) .
310 (lambda unrestricted value : Nat .
311 (let unrestricted quotient = (naturalDivideUnchecked value 10)
312 in (nat-eliminate
313 (lambda unrestricted nonzero : Nat . BytesBuilder)
314 (bytes-builder-chunk (bytes (nat-to-byte (naturalAdd 48 (naturalModuloUnchecked value 10)))))
315 (lambda unrestricted quotientPredecessor : Nat .
316 (lambda unrestricted quotientInduction : BytesBuilder .
317 (bytes-builder-append
318 (induction quotient)
319 (bytes-builder-chunk (bytes (nat-to-byte (naturalAdd 48 (naturalModuloUnchecked value 10))))))))
320 (naturalNonzero quotient))))))
321 fuel))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.