Zp
Testing a ``natural'' against 0
(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 =-comparison with 0.
Function: zp
(defun zp (x)
(declare (xargs :guard (and (integerp x) (<= 0 x))))
(if (integerp x) (<= x 0) t))
