Saturating subtraction over canonical digits. Compare before borrowing so
underflow produces canonical zero. All Nat arithmetic is bounded to 0..19;
the numeric value is never expanded to a unary natural.
298def magnitudeSubtractBorrow =
299 (lambda unrestricted digit : Byte .
300 (lambda unrestricted subtrahend : Nat . (nat-less-than (byte-to-nat digit) subtrahend)))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.