Zerop
Test an acl2-number against 0
(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.
Function: zerop
(defun zerop (x)
(declare (xargs :guard (acl2-numberp x)))
(eql x 0))
