		Search-engine friendly clone of the ACL2 documentation.

Vl-oddinfo

Vl-oddinfo-p

Recognizer for vl-oddinfo structures.

Signature
(vl-oddinfo-p x) → *

Definitions and Theorems

Function: vl-oddinfo-p

(defun vl-oddinfo-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'vl-oddinfo-p))
  (declare (ignorable __function__))
  (and
     (mbe :logic
          (and (alistp x)
               (equal (strip-cars x)
                      '(type subexpr simple complex swidth cwidth)))
          :exec (fty::alist-with-carsp
                     x
                     '(type subexpr simple complex swidth cwidth)))
     (b* ((type (cdr (std::da-nth 0 x)))
          (subexpr (cdr (std::da-nth 1 x)))
          (simple (cdr (std::da-nth 2 x)))
          (complex (cdr (std::da-nth 3 x)))
          (swidth (cdr (std::da-nth 4 x)))
          (cwidth (cdr (std::da-nth 5 x))))
       (and (symbolp type)
            (vl-expr-p subexpr)
            (vl-expr-p simple)
            (vl-expr-p complex)
            (maybe-natp swidth)
            (maybe-natp cwidth))))))

Theorem: consp-when-vl-oddinfo-p

(defthm consp-when-vl-oddinfo-p
  (implies (vl-oddinfo-p x) (consp x))
  :rule-classes :compound-recognizer)