Source/Packages

Compiler.NaturalMagnitudeArithmetic

packages/compiler/src/Compiler/NaturalMagnitudeArithmetic.alpha

592 lines29 declarations28.9 KiBSHA-256 9c904be71be4

def · lines 298–300

magnitudeSubtractBorrow

Full file
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.