		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Zp-listp

Recognize true lists of zp values.

Signature
(zp-listp x) → std::bool

A value satisfies zp iff it does not satisfy posp.

We use the :negatedp feature of std::deflist because using zp (without :negatedp) causes a guard violation.

Definitions and Theorems

Function: zp-listp

(defun zp-listp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'zp-listp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (not (posp (car x)))
             (zp-listp (cdr x)))
      (null x))))

Subtopics

Zp-listp-basics: Basic theorems about zp-listp, generated by std::deflist.