		Search-engine friendly clone of the ACL2 documentation.

Vex-p

Signature
(vex-p x) → *

Definitions and Theorems

Function: vex-p

(defun vex-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vex-p))
    (declare (ignorable __function__))
    (and (true-listp x)
         (subsetp-equal x *vex-pfx-cases*)
         (no-duplicatesp-equal x)
         (avx-pfx-well-formed-p x t))))