		Search-engine friendly clone of the ACL2 documentation.

R-eqlable-alistp

Recognizer for a true list of pairs whose cdrs are suitable for eql

The predicate r-eqlable-alistp tests whether its argument is a true-listp of consp objects whose cdrs all satisfy eqlablep.

Function: r-eqlable-alistp

(defun r-eqlable-alistp (x)
  (declare (xargs :guard t))
  (cond ((atom x) (equal x nil))
        (t (and (consp (car x))
                (eqlablep (cdr (car x)))
                (r-eqlable-alistp (cdr x))))))