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