Four little-endian bytes as a natural, with the remaining input. A shorter
input is reported as truncated, never padded.
149def stdCodecDecodeWord32 =
150 (lambda unrestricted input : Bytes .
151 (eliminate
152 StdBool
153 (lambda unrestricted current : (family StdBool) . (family StdDecoded Nat))
154 (stdBoolFromNatural (nat-less-than (bytes-length input) (byte-to-nat (byte 4))))
155 (branch StdTrue . (constructor StdDecoded StdDecodedTruncated Nat))
156 (branch
157 StdFalse
158 .
159 (let unrestricted byte0 =
160 (byte-to-nat (bytes-head input))
161 in
162 (let unrestricted after0 =
163 (bytes-tail input)
164 in
165 (let unrestricted byte1 =
166 (byte-to-nat (bytes-head after0))
167 in
168 (let unrestricted after1 =
169 (bytes-tail after0)
170 in
171 (let unrestricted byte2 =
172 (byte-to-nat (bytes-head after1))
173 in
174 (let unrestricted after2 =
175 (bytes-tail after1)
176 in
177 (let unrestricted byte3 =
178 (byte-to-nat (bytes-head after2))
179 in
180 (constructor
181 StdDecoded
182 StdDecodedValue
183 Nat
184 (naturalAdd
185 byte0
186 (naturalMultiply
187 stdCodecByteBase
188 (naturalAdd
189 byte1
190 (naturalMultiply
191 stdCodecByteBase
192 (naturalAdd byte2 (naturalMultiply stdCodecByteBase byte3))))))
193 (bytes-tail after2))))))))))))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.