455def dataBytesSlice =
456 (lambda unrestricted input : Bytes .
457 (lambda unrestricted offset : Nat .
458 (lambda unrestricted requestedLength : Nat .
459 (app
460 (lambda unrestricted inputLength : Nat .
461 (nat-eliminate
462 (lambda unrestricted current : Nat . (family DataBytesSliceResult))
463 (constructor
464 DataBytesSliceResult
465 DataBytesSliceFailed
466 (constructor DataBytesErrorCode DataBytesOffsetOutOfRange)
467 (dataBytesTelemetry
468 inputLength
469 requestedLength
470 zero
471 zero
472 zero
473 zero
474 zero
475 inputLength))
476 (lambda unrestricted offsetFitsPredecessor : Nat .
477 (lambda unrestricted offsetFitsInduction : (family DataBytesSliceResult) .
478 (nat-eliminate
479 (lambda unrestricted current : Nat . (family DataBytesSliceResult))
480 (constructor
481 DataBytesSliceResult
482 DataBytesSliceFailed
483 (constructor DataBytesErrorCode DataBytesSliceOutOfRange)
484 (dataBytesTelemetry
485 inputLength
486 requestedLength
487 zero
488 zero
489 zero
490 zero
491 offset
492 inputLength))
493 (lambda unrestricted lengthFitsPredecessor : Nat .
494 (lambda unrestricted lengthFitsInduction : (family DataBytesSliceResult) .
495 (constructor
496 DataBytesSliceResult
497 DataBytesSliceSucceeded
498 (constructor
499 DataBytesSlice
500 DataBytesSliceView
501 (dataBytesDropValidated offset input)
502 requestedLength)
503 (dataBytesTelemetry
504 inputLength
505 requestedLength
506 zero
507 zero
508 requestedLength
509 zero
510 offset
511 inputLength))))
512 (naturalLessOrEqual
513 requestedLength
514 (naturalSaturatingSubtract inputLength offset)))))
515 (naturalLessOrEqual offset inputLength)))
516 (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.