a recognizer for the natural numbers
Major Section:  ACL2-BUILT-INS

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. We recommend the community book books/arithmetic/natp-posp.lisp as a book for reasoning about posp and natp. This book is included by community books books/arithmetic/top and books/arithmetic/top-with-meta.

To see the ACL2 definition of this function, see pf.