		Search-engine friendly clone of the ACL2 documentation.

Eqlable-alistp

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

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

Function: eqlable-alistp

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