ZP

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.