Major Section: ACL2-BUILT-INS

`(Zp n)`

is logically equivalent to `(equal (nfix n) 0)`

and is
the preferred termination test for recursion down the natural
numbers. `(Zp n)`

returns `t`

if `n`

is `0`

or not a natural
number; it returns `nil`

otherwise. Thus, in the ACL2 logic
(ignoring the issue of guards):

n (zp n) 3 nil 0 t -1 t 5/2 t #c(1 3) t 'abc t

`(Zp n)`

has a guard requiring `n`

to be a natural number.

For a discussion of the various idioms for testing against `0`

,
see zero-test-idioms.

`Zp`

is typically used as the termination test in recursions down
the natural numbers. It has the advantage of ``coercing'' its
argument to a natural and hence allows the definition to be admitted
without an explicit type check in the body. Guard verification
allows `zp`

to be compiled as a direct `=`

-comparision with `0`

.