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)))
Subtopics
- Maybe-natp
- Recognizer for naturals and nil.
