## ZEROP

test an acl2-number against 0
```Major Section:  PROGRAMMING
```

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

## ZIP

testing an ``integer'' against 0
```Major Section:  PROGRAMMING
```

`(Zip i)` is logically equivalent to `(equal (ifix i) 0)` and is the preferred termination test for recursion through the integers. `(Zip i)` returns `t` if `i` is `0` or not an integer; it returns `nil` otherwise. Thus,

```    i       (zp i)
3         nil
0         t
-2        nil
5/2       t
#c(1 3)   t
'abc      t
```

`(Zip i)` has a guard requiring `i` to be an integer.

For a discussion of the various idioms for testing against `0`, see zero-test-idioms.

`Zip` is typically used as the termination test in recursions through the integers. It has the advantage of ``coercing'' its argument to an integer and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows `zip` to be compiled as a direct `=`-comparision with `0`.

## ZP

testing a ``natural'' against 0
```Major Section:  PROGRAMMING
```

`(Zp n)` is logically equivalent to `(equal (nfix n) 0)` and is the preferred termination test for recursion down the natural numbers. `(Zp n)` returns `t` if `n` is `0` or not a natural number; it returns `nil` otherwise. Thus, in the ACL2 logic (ignoring the issue of guards):

```    n       (zp n)
3         nil
0         t
-1        t
5/2       t
#c(1 3)   t
'abc      t
```

`(Zp n)` has a guard requiring `n` to be a natural number.

For a discussion of the various idioms for testing against `0`, see zero-test-idioms.

`Zp` is typically used as the termination test in recursions down the natural numbers. It has the advantage of ``coercing'' its argument to a natural and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows `zp` to be compiled as a direct `=`-comparision with `0`.