a natural as eight little-endian bytes (it is below 2^64)
148def checkpointEnvelopeWord =
149 (lambda unrestricted value : Nat .
150 (bytes-builder-build
151 (app (nat-eliminate
152 (lambda unrestricted current : Nat . (pi unrestricted rest : Nat . BytesBuilder))
153 (lambda unrestricted rest : Nat . (bytes-builder-chunk b""))
154 (lambda unrestricted p : Nat .
155 (lambda unrestricted induction : (pi unrestricted rest : Nat . BytesBuilder) .
156 (lambda unrestricted rest : Nat .
157 (bytes-builder-append
158 (bytes-builder-chunk (bytes (nat-to-byte (naturalModuloUnchecked rest 256))))
159 (induction (naturalDivideUnchecked rest 256))))))
160 8)
161 value)))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.