ZEROP

Major Section:  PROGRAMMING

(zerop x) is t if x is 0 and is nil otherwise. Thus, it is logically equivalent to (equal x 0).

(Zerop x) has a guard requiring x to be numeric and can be expected to execute more efficiently than (equal x 0) in properly guarded compiled code.

In recursions down the natural numbers, (zp x) is preferred over (zerop x) because the former coerces x to a natural and allows the termination proof. In recursions through the integers, (zip x) is preferred. See zero-test-idioms.

Zerop is a Common Lisp function. See any Common Lisp documentation for more information.

ZIP

Major Section:  PROGRAMMING

(Zip i) is logically equivalent to (equal (ifix i) 0) and is the preferred termination test for recursion through the integers. (Zip i) returns t if i is 0 or not an integer; it returns nil otherwise. Thus,

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

(Zip i) has a guard requiring i to be an integer.

For a discussion of the various idioms for testing against 0, see zero-test-idioms.

Zip is typically used as the termination test in recursions through the integers. It has the advantage of ``coercing'' its argument to an integer and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows zip to be compiled as a direct =-comparision with 0.

ZP

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.