Check before addition. Runtime Nat is machine-sized, so a post-add check could
observe a wrapped value and is not acceptable.
270def dataBytesCheckedAddWithin =
271 (lambda unrestricted limit : Nat .
272 (lambda unrestricted failure : (family DataBytesErrorCode) .
273 (lambda unrestricted left : Nat .
274 (lambda unrestricted right : Nat .
275 (nat-eliminate
276 (lambda unrestricted current : Nat . (family DataBytesCheckedNaturalResult))
277 (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalFailed failure)
278 (lambda unrestricted leftFitsPredecessor : Nat .
279 (lambda unrestricted leftFitsInduction : (family DataBytesCheckedNaturalResult) .
280 (nat-eliminate
281 (lambda unrestricted current : Nat . (family DataBytesCheckedNaturalResult))
282 (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalFailed failure)
283 (lambda unrestricted rightFitsPredecessor : Nat .
284 (lambda unrestricted rightFitsInduction : (family DataBytesCheckedNaturalResult) .
285 (constructor
286 DataBytesCheckedNaturalResult
287 DataBytesCheckedNaturalSucceeded
288 (naturalAdd left right))))
289 (naturalLessOrEqual right (naturalSaturatingSubtract limit left)))))
290 (naturalLessOrEqual left limit))))))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.