Major Section: ACL2-BUILT-INS
(zerop 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.