953def dataBytesAppendWithin =
954 (lambda unrestricted allocationLimit : Nat .
955 (lambda unrestricted left : Bytes .
956 (lambda unrestricted right : Bytes .
957 (app
958 (lambda unrestricted leftLength : Nat .
959 (app
960 (lambda unrestricted rightLength : Nat .
961 (eliminate
962 DataBytesCheckedNaturalResult
963 (lambda unrestricted current : (family DataBytesCheckedNaturalResult) .
964 (family DataBytesResult))
965 (dataBytesCheckedAddWithin
966 allocationLimit
967 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
968 leftLength
969 rightLength)
970 (branch
971 DataBytesCheckedNaturalSucceeded
972 totalLength
973 .
974 (app
975 (lambda unrestricted output : Bytes .
976 (constructor
977 DataBytesResult
978 DataBytesSucceeded
979 output
980 (dataBytesTelemetry
981 totalLength
982 totalLength
983 totalLength
984 dataBytesNaturalTwo
985 totalLength
986 zero
987 totalLength
988 allocationLimit)))
989 (bytes-builder-build
990 (bytes-builder-append
991 (bytes-builder-chunk left)
992 (bytes-builder-chunk right)))))
993 (branch
994 DataBytesCheckedNaturalFailed
995 code
996 .
997 (constructor
998 DataBytesResult
999 DataBytesFailed
1000 code
1001 (dataBytesTelemetry
1002 leftLength
1003 rightLength
1004 zero
1005 zero
1006 zero
1007 zero
1008 zero
1009 allocationLimit)))))
1010 (bytes-length right)))
1011 (bytes-length left)))))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.