a recognizer for the positive integers
Major Section:  ACL2-BUILT-INS

(posp x) is logically equivalent to (not (zp x)) (see zp) and also to (and (natp x) (not (equal x 0))). We recommend the community book books/ordinals/natp-posp 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.