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.

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`

.

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`

.