### NATP

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.