1240def dataBytesWord32ExactFromStream =
1241 (lambda unrestricted inputLength : Nat .
1242 (lambda unrestricted decoded : (family DataBytesWord32DecodeResult) .
1243 (eliminate
1244 DataBytesWord32DecodeResult
1245 (lambda unrestricted current : (family DataBytesWord32DecodeResult) .
1246 (family DataBytesWord32ExactDecodeResult))
1247 decoded
1248 (branch
1249 DataBytesWord32Decoded
1250 value
1251 remaining
1252 .
1253 (constructor
1254 DataBytesWord32ExactDecodeResult
1255 DataBytesWord32ExactlyDecoded
1256 value
1257 (dataBytesTelemetry
1258 inputLength
1259 dataBytesNaturalFour
1260 dataBytesNaturalFour
1261 dataBytesNaturalOne
1262 inputLength
1263 zero
1264 dataBytesNaturalFour
1265 dataBytesNaturalFour)))
1266 (branch DataBytesWord32DecodeFailed code . (dataBytesWord32ExactFailure inputLength)))))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.