Major Section: PROGRAMMING
(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.
