1335def dataBytesDecodeWord64BEExact =
1336 (lambda unrestricted input : Bytes .
1337 (app
1338 (lambda unrestricted inputLength : Nat .
1339 (nat-eliminate
1340 (lambda unrestricted current : Nat . (family DataBytesWord64ExactDecodeResult))
1341 (dataBytesWord64ExactFailure inputLength)
1342 (lambda unrestricted exactPredecessor : Nat .
1343 (lambda unrestricted exactInduction : (family DataBytesWord64ExactDecodeResult) .
1344 (dataBytesWord64ExactFromStream inputLength (dataBytesReadWord64BE input))))
1345 (naturalEqual inputLength dataBytesNaturalEight)))
1346 (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.