1268def dataBytesWord64ExactFromStream =
1269 (lambda unrestricted inputLength : Nat .
1270 (lambda unrestricted decoded : (family DataBytesWord64DecodeResult) .
1271 (eliminate
1272 DataBytesWord64DecodeResult
1273 (lambda unrestricted current : (family DataBytesWord64DecodeResult) .
1274 (family DataBytesWord64ExactDecodeResult))
1275 decoded
1276 (branch
1277 DataBytesWord64Decoded
1278 value
1279 remaining
1280 .
1281 (constructor
1282 DataBytesWord64ExactDecodeResult
1283 DataBytesWord64ExactlyDecoded
1284 value
1285 (dataBytesTelemetry
1286 inputLength
1287 dataBytesNaturalEight
1288 dataBytesNaturalEight
1289 dataBytesNaturalOne
1290 inputLength
1291 zero
1292 dataBytesNaturalEight
1293 dataBytesNaturalEight)))
1294 (branch DataBytesWord64DecodeFailed code . (dataBytesWord64ExactFailure 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.