1309def dataBytesDecodeWord32BEExact =
1310 (lambda unrestricted input : Bytes .
1311 (app
1312 (lambda unrestricted inputLength : Nat .
1313 (nat-eliminate
1314 (lambda unrestricted current : Nat . (family DataBytesWord32ExactDecodeResult))
1315 (dataBytesWord32ExactFailure inputLength)
1316 (lambda unrestricted exactPredecessor : Nat .
1317 (lambda unrestricted exactInduction : (family DataBytesWord32ExactDecodeResult) .
1318 (dataBytesWord32ExactFromStream inputLength (dataBytesReadWord32BE input))))
1319 (naturalEqual inputLength dataBytesNaturalFour)))
1320 (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.