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.
