ZIP

Major Section:  ACL2-BUILT-INS

(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         (zip 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.