1296def dataBytesDecodeWord32LEExact =
1297 (lambda unrestricted input : Bytes .
1298 (app
1299 (lambda unrestricted inputLength : Nat .
1300 (nat-eliminate
1301 (lambda unrestricted current : Nat . (family DataBytesWord32ExactDecodeResult))
1302 (dataBytesWord32ExactFailure inputLength)
1303 (lambda unrestricted exactPredecessor : Nat .
1304 (lambda unrestricted exactInduction : (family DataBytesWord32ExactDecodeResult) .
1305 (dataBytesWord32ExactFromStream inputLength (dataBytesReadWord32LE input))))
1306 (naturalEqual inputLength dataBytesNaturalFour)))
1307 (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.