Batch single-byte repetitions into 4096-byte chunks. This is a construction
granularity, not a maximum extent: quotient and remainder cover all bytes.
360def dataBytesRepeatByte = (lambda unrestricted value : Byte . (lambda unrestricted count : Nat .
361 (let unrestricted single = (bytes-cons value b"") in
362 (nat-eliminate (lambda unrestricted small : Nat . Bytes)
363 (let unrestricted block = (dataBytesRepeat single 4096) in
364 (bytes-append (dataBytesRepeat block (naturalDivideUnchecked count 4096))
365 (dataBytesRepeat single (naturalModuloUnchecked count 4096))))
366 (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Bytes .
367 (dataBytesRepeat single count)))
368 (nat-less-than count 4096)))))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.