866def dataBytesBuilderBuildWithin =
867 (lambda unrestricted allocationLimit : Nat .
868 (lambda unrestricted builder : (family DataBytesBuilder) .
869 (eliminate
870 DataBytesBuilder
871 (lambda unrestricted current : (family DataBytesBuilder) . (family DataBytesResult))
872 builder
873 (branch
874 DataBytesBuilderValue
875 runtime
876 length
877 chunks
878 shared
879 copied
880 .
881 (nat-eliminate
882 (lambda unrestricted current : Nat . (family DataBytesResult))
883 (constructor
884 DataBytesResult
885 DataBytesFailed
886 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
887 (dataBytesZeroTelemetry allocationLimit))
888 (lambda unrestricted validPredecessor : Nat .
889 (lambda unrestricted validInduction : (family DataBytesResult) .
890 (nat-eliminate
891 (lambda unrestricted current : Nat . (family DataBytesResult))
892 (constructor
893 DataBytesResult
894 DataBytesFailed
895 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
896 (dataBytesTelemetry
897 length
898 length
899 zero
900 chunks
901 shared
902 copied
903 zero
904 allocationLimit))
905 (lambda unrestricted fitsPredecessor : Nat .
906 (lambda unrestricted fitsInduction : (family DataBytesResult) .
907 (app
908 (lambda unrestricted output : Bytes .
909 (nat-eliminate
910 (lambda unrestricted current : Nat . (family DataBytesResult))
911 (constructor
912 DataBytesResult
913 DataBytesFailed
914 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
915 (dataBytesTelemetry
916 length
917 length
918 zero
919 chunks
920 shared
921 copied
922 length
923 allocationLimit))
924 (lambda unrestricted exactPredecessor : Nat .
925 (lambda unrestricted exactInduction : (family DataBytesResult) .
926 (constructor
927 DataBytesResult
928 DataBytesSucceeded
929 output
930 (dataBytesTelemetry
931 length
932 length
933 length
934 chunks
935 shared
936 copied
937 length
938 allocationLimit))))
939 (naturalEqual (bytes-length output) length)))
940 (bytes-builder-build runtime))))
941 (naturalLessOrEqual length allocationLimit))))
942 (dataBytesBuilderMetadataValid length chunks shared copied))))))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.