		Search-engine friendly clone of the ACL2 documentation.

Defstruct-member-info

Defstruct-member-infop

Recognizer for defstruct-member-info structures.

Signature
(defstruct-member-infop x) → *

Definitions and Theorems

Function: defstruct-member-infop

(defun defstruct-member-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'defstruct-member-infop))
  (declare (ignorable __function__))
  (and
     (mbe :logic
          (and (alistp x)
               (equal (strip-cars x)
                      '(memtype reader
                                reader-element writer writer-element
                                checker length reader-return-thm
                                reader-element-return-thm
                                writer-return-thm
                                writer-element-return-thm)))
          :exec (fty::alist-with-carsp
                     x
                     '(memtype reader
                               reader-element writer writer-element
                               checker length reader-return-thm
                               reader-element-return-thm
                               writer-return-thm
                               writer-element-return-thm)))
     (b* ((memtype (cdr (std::da-nth 0 x)))
          (reader (cdr (std::da-nth 1 x)))
          (reader-element (cdr (std::da-nth 2 x)))
          (writer (cdr (std::da-nth 3 x)))
          (writer-element (cdr (std::da-nth 4 x)))
          (checker (cdr (std::da-nth 5 x)))
          (length (cdr (std::da-nth 6 x)))
          (reader-return-thm (cdr (std::da-nth 7 x)))
          (reader-element-return-thm (cdr (std::da-nth 8 x)))
          (writer-return-thm (cdr (std::da-nth 9 x)))
          (writer-element-return-thm (cdr (std::da-nth 10 x))))
       (and (member-typep memtype)
            (symbolp reader)
            (symbolp reader-element)
            (symbolp writer)
            (symbolp writer-element)
            (symbolp checker)
            (symbolp length)
            (symbolp reader-return-thm)
            (symbolp reader-element-return-thm)
            (symbolp writer-return-thm)
            (symbolp writer-element-return-thm))))))

Theorem: consp-when-defstruct-member-infop

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