		Search-engine friendly clone of the ACL2 documentation.

Natp

A recognizer for the natural numbers

The natural numbers is the set of all non-negative integers, {0,1,2,3,...}. Natp returns t if and only its argument is a natural number, and nil otherwise.

The community book arithmetic/natp-posp has some lightweight rules for reasoning about posp and natp, and is included in the arithmetic-1 library. For a somewhat heavier and more comprehensive alternative, you may wish to instead see the arith-equivs book.

Function: natp

(defun natp (x)
       (declare (xargs :guard t))
       (and (integerp x) (<= 0 x)))