417def dataBytesIndex =
418 (lambda unrestricted input : Bytes .
419 (lambda unrestricted index : Nat .
420 (app
421 (lambda unrestricted inputLength : Nat .
422 (nat-eliminate
423 (lambda unrestricted current : Nat . (family DataBytesIndexResult))
424 (constructor
425 DataBytesIndexResult
426 DataBytesIndexFailed
427 (constructor DataBytesErrorCode DataBytesIndexOutOfRange)
428 (dataBytesTelemetry
429 inputLength
430 dataBytesNaturalOne
431 zero
432 zero
433 zero
434 zero
435 index
436 inputLength))
437 (lambda unrestricted fitsPredecessor : Nat .
438 (lambda unrestricted fitsInduction : (family DataBytesIndexResult) .
439 (constructor
440 DataBytesIndexResult
441 DataBytesIndexSucceeded
442 (dataBytesByteAtValidated input index)
443 (dataBytesTelemetry
444 inputLength
445 dataBytesNaturalOne
446 dataBytesNaturalOne
447 zero
448 dataBytesNaturalOne
449 zero
450 index
451 inputLength))))
452 (naturalLess index inputLength)))
453 (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.