Subtract only after retaining the offset bound. This is equivalent to
offset + width <= extent over naturals, without overflowing machine-word
evaluation when a rejected caller supplies a maximal offset or width.
104def telemetryRangeFits =
105 (lambda unrestricted offset : Nat .
106 (lambda unrestricted width : Nat .
107 (lambda unrestricted extent : Nat .
108 (naturalAnd
109 (naturalLessOrEqual offset extent)
110 (naturalLessOrEqual width (naturalSaturatingSubtract extent offset))))))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.