The flag operations below are written on the primitives themselves, not
on one another: a realization calls them millions of times, and each call
of one helper from another costs the machine an application chain (an
equality through naturalAnd, naturalIsZero and naturalSelect took 44 steps
where these take a handful; they were three fifths of realizing a tiled
product). Each eliminates only a 0/1 flag from nat-less-than.
79def naturalAnd =
80 (lambda unrestricted left : Nat .
81 (lambda unrestricted right : Nat .
82 (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (nat-less-than zero right))) (nat-less-than zero left))))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.