		Search-engine friendly clone of the ACL2 documentation.

Vl-unparam-ledger

Vl-unparam-ledger-p

Recognizer for vl-unparam-ledger structures.

Signature
(vl-unparam-ledger-p x) → *

Definitions and Theorems

Function: vl-unparam-ledger-p

(defun vl-unparam-ledger-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'vl-unparam-ledger-p))
  (declare (ignorable __function__))
  (and
   (mbe
      :logic (and (alistp x)
                  (equal (strip-cars x)
                         '(ndb instkeymap omit-default-params)))
      :exec
      (fty::alist-with-carsp x
                             '(ndb instkeymap omit-default-params)))
   (b* ((ndb (cdr (std::da-nth 0 x)))
        (instkeymap (cdr (std::da-nth 1 x)))
        (omit-default-params (cdr (std::da-nth 2 x))))
     (and (vl-namedb-p ndb)
          (vl-unparam-instkeymap-p instkeymap)
          (booleanp omit-default-params))))))

Theorem: consp-when-vl-unparam-ledger-p

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