D21: the arithmetic below is the language's own (`nat-add` and friends run in
one machine operation at run time and fold at compile time); the folds that
counted step by step are gone. Semantics are unchanged: subtraction
saturates at zero, x / 0 = 0, x mod 0 = x.
93def naturalAdd =
94 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-add left right)))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.