1322def dataBytesDecodeWord64LEExact =
1323 (lambda unrestricted input : Bytes .
1324 (app
1325 (lambda unrestricted inputLength : Nat .
1326 (nat-eliminate
1327 (lambda unrestricted current : Nat . (family DataBytesWord64ExactDecodeResult))
1328 (dataBytesWord64ExactFailure inputLength)
1329 (lambda unrestricted exactPredecessor : Nat .
1330 (lambda unrestricted exactInduction : (family DataBytesWord64ExactDecodeResult) .
1331 (dataBytesWord64ExactFromStream inputLength (dataBytesReadWord64LE input))))
1332 (naturalEqual inputLength dataBytesNaturalEight)))
1333 (bytes-length input)))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.