		Search-engine friendly clone of the ACL2 documentation.

Defobject-info

Defobject-infop

Recognizer for defobject-info structures.

Signature
(defobject-infop x) → *

Definitions and Theorems

Function: defobject-infop

(defun defobject-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'defobject-infop))
  (declare (ignorable __function__))
  (and
   (mbe
    :logic
    (and
        (alistp x)
        (equal (strip-cars x)
               '(name-ident name-symbol
                            type init recognizer initializer call)))
    :exec (fty::alist-with-carsp
               x
               '(name-ident name-symbol
                            type init recognizer initializer call)))
   (b* ((name-ident (cdr (std::da-nth 0 x)))
        (name-symbol (cdr (std::da-nth 1 x)))
        (type (cdr (std::da-nth 2 x)))
        (init (cdr (std::da-nth 3 x)))
        (recognizer (cdr (std::da-nth 4 x)))
        (initializer (cdr (std::da-nth 5 x)))
        (call (cdr (std::da-nth 6 x))))
     (and (identp name-ident)
          (symbolp name-symbol)
          (typep type)
          (initer-optionp init)
          (symbolp recognizer)
          (symbolp initializer)
          (pseudo-event-formp call))))))

Theorem: consp-when-defobject-infop

(defthm consp-when-defobject-infop
  (implies (defobject-infop x) (consp x))
  :rule-classes :compound-recognizer)