		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-p

Signature
(s4vec-p x) → *

Definitions and Theorems

Function: s4vec-p

(defun s4vec-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 's4vec-p))
    (declare (ignorable __function__))
    (or (integerp x)
        (and (consp x)
             (sparseint-p (car x))
             (or (and (not (cdr x))
                      (not (integerp (car x))))
                 (and (sparseint-p (cdr x))
                      (not (equal (car x) (cdr x)))))))))