Major Section: ACL2-BUILT-INS

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

To see the ACL2 definition of this function, see pf.