Major Section: ACL2-BUILT-INS
The natural numbers is the set of all non-negative integers,
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
natp. This book is included by community books
To see the ACL2 definition of this function, see pf.