Build the prefix once. Repeated bytes-cons copies every growing suffix in
the native evaluator, making a large imported normalization table quadratic.
A builder retains each byte as a chunk and materializes the prefix linearly.
Keep the total helper's old zero-padding behavior past the end; public
bounded slices reject those requests before calling this helper.
318def dataBytesTakeBuilder =
319 (lambda unrestricted count : Nat .
320 (nat-eliminate
321 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . BytesBuilder))
322 (lambda unrestricted input : Bytes . (bytes-builder-empty))
323 (lambda unrestricted predecessor : Nat .
324 (lambda unrestricted induction : (pi unrestricted input : Bytes . BytesBuilder) .
325 (lambda unrestricted input : Bytes .
326 (bytes-builder-append
327 (bytes-builder-chunk (bytes-cons (bytes-head input) b""))
328 (induction (bytes-tail input))))))
329 count))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.