		Search-engine friendly clone of the ACL2 documentation.

Avx-pfx-well-formed-p

Signature
(avx-pfx-well-formed-p lst vex?) → *
Arguments: lst — Guard (true-listp lst).; vex? — Guard (booleanp vex?).

Definitions and Theorems

Function: avx-pfx-well-formed-p

(defun avx-pfx-well-formed-p (lst vex?)
  (declare (xargs :guard (and (true-listp lst) (booleanp vex?))))
  (let ((__function__ 'avx-pfx-well-formed-p))
    (declare (ignorable __function__))
    (b* ((count-alst (count-avx-pfx-cases lst nil vex?))
         (vvvv (if (consp (assoc-equal :vvvv count-alst))
                   (cdr (assoc-equal :vvvv count-alst))
                 0))
         ((unless (and (natp vvvv) (<= vvvv 1)))
          (cw "Duplicates encountered in VVVV! Lst: ~p0~%"
              lst))
         (l (if (consp (assoc-equal :l count-alst))
                (cdr (assoc-equal :l count-alst))
              0))
         ((unless (and (natp l) (<= l 1)))
          (cw "Duplicates encountered in L! Lst: ~p0~%"
              lst))
         (pp (if (consp (assoc-equal :pp count-alst))
                 (cdr (assoc-equal :pp count-alst))
               0))
         ((unless (and (natp pp) (<= pp 1)))
          (cw "Duplicates encountered in PP! Lst: ~p0~%"
              lst))
         (mm (if (consp (assoc-equal :mm count-alst))
                 (cdr (assoc-equal :mm count-alst))
               0))
         ((unless (equal mm 1))
          (cw "MM not equal to 1! Lst: ~p0~%" lst))
         (w (if (consp (assoc-equal :w count-alst))
                (cdr (assoc-equal :w count-alst))
              0))
         ((unless (and (natp w) (<= w 1)))
          (cw "Duplicates encountered in W! Lst: ~p0~%"
              lst)))
      t)))