604def dataBytesSliceIndex =
605 (lambda unrestricted slice : (family DataBytesSlice) .
606 (lambda unrestricted index : Nat .
607 (eliminate
608 DataBytesSlice
609 (lambda unrestricted current : (family DataBytesSlice) . (family DataBytesIndexResult))
610 slice
611 (branch
612 DataBytesSliceView
613 suffix
614 sliceLength
615 .
616 (app
617 (lambda unrestricted suffixLength : Nat .
618 (nat-eliminate
619 (lambda unrestricted current : Nat . (family DataBytesIndexResult))
620 (constructor
621 DataBytesIndexResult
622 DataBytesIndexFailed
623 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
624 (dataBytesTelemetry
625 suffixLength
626 dataBytesNaturalOne
627 zero
628 zero
629 zero
630 zero
631 zero
632 suffixLength))
633 (lambda unrestricted validPredecessor : Nat .
634 (lambda unrestricted validInduction : (family DataBytesIndexResult) .
635 (nat-eliminate
636 (lambda unrestricted current : Nat . (family DataBytesIndexResult))
637 (constructor
638 DataBytesIndexResult
639 DataBytesIndexFailed
640 (constructor DataBytesErrorCode DataBytesIndexOutOfRange)
641 (dataBytesTelemetry
642 sliceLength
643 dataBytesNaturalOne
644 zero
645 zero
646 zero
647 zero
648 index
649 sliceLength))
650 (lambda unrestricted fitsPredecessor : Nat .
651 (lambda unrestricted fitsInduction : (family DataBytesIndexResult) .
652 (constructor
653 DataBytesIndexResult
654 DataBytesIndexSucceeded
655 (dataBytesByteAtValidated suffix index)
656 (dataBytesTelemetry
657 sliceLength
658 dataBytesNaturalOne
659 dataBytesNaturalOne
660 zero
661 dataBytesNaturalOne
662 zero
663 index
664 sliceLength))))
665 (naturalLess index sliceLength))))
666 (naturalLessOrEqual sliceLength suffixLength)))
667 (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.