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
0 or not an integer; it
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
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
zip to be compiled as a direct