test an acl2-number against 0
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.