Source/Packages

Std.Codec

packages/foundation/standard/src/Std/Codec.alpha

221 lines16 declarations8.7 KiBSHA-256 660b0bd459e5

def · lines 117–145

stdCodecEncodeWord32

Full file
A natural as four little-endian bytes. Values wider than the field are reduced modulo the width, which is stated here rather than discovered: a caller who needs a checked conversion uses `Data.CheckedWord64`.
117def stdCodecEncodeWord32 =
118  (lambda unrestricted value : Nat .
119    (let unrestricted byte0 =
120      (naturalModuloUnchecked value stdCodecByteBase)
121      in
122      (let unrestricted rest1 =
123        (naturalDivideUnchecked value stdCodecByteBase)
124        in
125        (let unrestricted byte1 =
126          (naturalModuloUnchecked rest1 stdCodecByteBase)
127          in
128          (let unrestricted rest2 =
129            (naturalDivideUnchecked rest1 stdCodecByteBase)
130            in
131            (let unrestricted byte2 =
132              (naturalModuloUnchecked rest2 stdCodecByteBase)
133              in
134              (let unrestricted rest3 =
135                (naturalDivideUnchecked rest2 stdCodecByteBase)
136                in
137                (bytes-cons
138                  (nat-to-byte byte0)
139                  (bytes-cons
140                    (nat-to-byte byte1)
141                    (bytes-cons
142                      (nat-to-byte byte2)
143                      (bytes-cons
144                        (nat-to-byte (naturalModuloUnchecked rest3 stdCodecByteBase))
145                        b"")))))))))))

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.