745def dataBytesBuilderAppendCheckedValues =
746 (lambda unrestricted allocationLimit : Nat .
747 (lambda unrestricted leftRuntime : BytesBuilder .
748 (lambda unrestricted leftLength : Nat .
749 (lambda unrestricted leftChunks : Nat .
750 (lambda unrestricted leftShared : Nat .
751 (lambda unrestricted leftCopied : Nat .
752 (lambda unrestricted rightRuntime : BytesBuilder .
753 (lambda unrestricted rightLength : Nat .
754 (lambda unrestricted rightChunks : Nat .
755 (lambda unrestricted rightShared : Nat .
756 (lambda unrestricted rightCopied : Nat .
757 (eliminate
758 DataBytesCheckedNaturalResult
759 (lambda unrestricted current : (family DataBytesCheckedNaturalResult) .
760 (family DataBytesBuilderResult))
761 (dataBytesCheckedAddWithin
762 allocationLimit
763 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
764 leftLength
765 rightLength)
766 (branch
767 DataBytesCheckedNaturalSucceeded
768 totalLength
769 .
770 (constructor
771 DataBytesBuilderResult
772 DataBytesBuilderSucceeded
773 (constructor
774 DataBytesBuilder
775 DataBytesBuilderValue
776 (bytes-builder-append leftRuntime rightRuntime)
777 totalLength
778 (naturalAdd leftChunks rightChunks)
779 (naturalAdd leftShared rightShared)
780 (naturalAdd leftCopied rightCopied))
781 (dataBytesTelemetry
782 totalLength
783 totalLength
784 zero
785 (naturalAdd leftChunks rightChunks)
786 (naturalAdd leftShared rightShared)
787 (naturalAdd leftCopied rightCopied)
788 zero
789 allocationLimit)))
790 (branch
791 DataBytesCheckedNaturalFailed
792 code
793 .
794 (constructor
795 DataBytesBuilderResult
796 DataBytesBuilderFailed
797 code
798 (dataBytesTelemetry
799 leftLength
800 rightLength
801 zero
802 zero
803 zero
804 zero
805 zero
806 allocationLimit)))))))))))))))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.