		Search-engine friendly clone of the ACL2 documentation.

Vl-scopeinfo

Vl-scopeinfo-p

Recognizer for vl-scopeinfo structures.

Signature
(vl-scopeinfo-p x) → *

Definitions and Theorems

Function: vl-scopeinfo-p

(defun vl-scopeinfo-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'vl-scopeinfo-p))
  (declare (ignorable __function__))
  (and
    (consp x)
    (eq (car x) :vl-scopeinfo)
    (std::prod-consp (cdr x))
    (std::prod-consp (std::prod-car (cdr x)))
    (std::prod-consp (std::prod-cdr (cdr x)))
    (std::prod-consp (std::prod-cdr (std::prod-cdr (cdr x))))
    (b*
     ((locals (std::prod-car (std::prod-car (cdr x))))
      (imports (std::prod-cdr (std::prod-car (cdr x))))
      (star-packages (std::prod-car (std::prod-cdr (cdr x))))
      (id (std::prod-car (std::prod-cdr (std::prod-cdr (cdr x)))))
      (scopetype
           (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x))))))
     (and (vl-scopeitem-alist-p locals)
          (vl-importresult-alist-p imports)
          (string-listp star-packages)
          (vl-maybe-scopeid-p id)
          (vl-scopetype-p scopetype))))))

Theorem: consp-when-vl-scopeinfo-p

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

Subtopics

Vl-scopeinfo-make-fast: Ensure that the fast alists in a vl-scopeinfo are indeed fast alists.