518def dataBytesSliceToBytesWithin =
519 (lambda unrestricted allocationLimit : Nat .
520 (lambda unrestricted slice : (family DataBytesSlice) .
521 (eliminate
522 DataBytesSlice
523 (lambda unrestricted current : (family DataBytesSlice) . (family DataBytesResult))
524 slice
525 (branch
526 DataBytesSliceView
527 suffix
528 requestedLength
529 .
530 (app
531 (lambda unrestricted suffixLength : Nat .
532 (nat-eliminate
533 (lambda unrestricted current : Nat . (family DataBytesResult))
534 (constructor
535 DataBytesResult
536 DataBytesFailed
537 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
538 (dataBytesTelemetry
539 suffixLength
540 requestedLength
541 zero
542 zero
543 zero
544 zero
545 zero
546 allocationLimit))
547 (lambda unrestricted validPredecessor : Nat .
548 (lambda unrestricted validInduction : (family DataBytesResult) .
549 (nat-eliminate
550 (lambda unrestricted current : Nat . (family DataBytesResult))
551 (constructor
552 DataBytesResult
553 DataBytesFailed
554 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
555 (dataBytesTelemetry
556 suffixLength
557 requestedLength
558 zero
559 zero
560 requestedLength
561 zero
562 zero
563 allocationLimit))
564 (lambda unrestricted limitPredecessor : Nat .
565 (lambda unrestricted limitInduction : (family DataBytesResult) .
566 (nat-eliminate
567 (lambda unrestricted current : Nat . (family DataBytesResult))
568 (constructor
569 DataBytesResult
570 DataBytesSucceeded
571 (dataBytesTakeValidated requestedLength suffix)
572 (dataBytesTelemetry
573 suffixLength
574 requestedLength
575 requestedLength
576 dataBytesNaturalOne
577 zero
578 requestedLength
579 requestedLength
580 allocationLimit))
581 (lambda unrestricted wholePredecessor : Nat .
582 (lambda unrestricted wholeInduction : (family DataBytesResult) .
583 (constructor
584 DataBytesResult
585 DataBytesSucceeded
586 suffix
587 (dataBytesTelemetry
588 suffixLength
589 requestedLength
590 requestedLength
591 dataBytesNaturalOne
592 requestedLength
593 zero
594 zero
595 allocationLimit))))
596 (naturalEqual requestedLength suffixLength))))
597 (naturalLessOrEqual requestedLength allocationLimit))))
598 (naturalLessOrEqual requestedLength suffixLength)))
599 (bytes-length suffix))))))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.