808def dataBytesBuilderAppendWithin =
809 (lambda unrestricted allocationLimit : Nat .
810 (lambda unrestricted left : (family DataBytesBuilder) .
811 (lambda unrestricted right : (family DataBytesBuilder) .
812 (eliminate
813 DataBytesBuilder
814 (lambda unrestricted current : (family DataBytesBuilder) .
815 (family DataBytesBuilderResult))
816 left
817 (branch
818 DataBytesBuilderValue
819 leftRuntime
820 leftLength
821 leftChunks
822 leftShared
823 leftCopied
824 .
825 (eliminate
826 DataBytesBuilder
827 (lambda unrestricted current : (family DataBytesBuilder) .
828 (family DataBytesBuilderResult))
829 right
830 (branch
831 DataBytesBuilderValue
832 rightRuntime
833 rightLength
834 rightChunks
835 rightShared
836 rightCopied
837 .
838 (nat-eliminate
839 (lambda unrestricted current : Nat . (family DataBytesBuilderResult))
840 (constructor
841 DataBytesBuilderResult
842 DataBytesBuilderFailed
843 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
844 (dataBytesZeroTelemetry allocationLimit))
845 (lambda unrestricted validPredecessor : Nat .
846 (lambda unrestricted validInduction : (family DataBytesBuilderResult) .
847 (dataBytesBuilderAppendCheckedValues
848 allocationLimit
849 leftRuntime
850 leftLength
851 leftChunks
852 leftShared
853 leftCopied
854 rightRuntime
855 rightLength
856 rightChunks
857 rightShared
858 rightCopied)))
859 (naturalAnd
860 (dataBytesBuilderMetadataValid leftLength leftChunks leftShared leftCopied)
861 (dataBytesBuilderMetadataValid rightLength rightChunks rightShared rightCopied))))))))))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.