		Search-engine friendly clone of the ACL2 documentation.

Defstruct-info

Defstruct-infop

Recognizer for defstruct-info structures.

Signature
(defstruct-infop x) → *

Definitions and Theorems

Function: defstruct-infop

(defun defstruct-infop (x)
 (declare (xargs :guard t))
 (let ((__function__ 'defstruct-infop))
  (declare (ignorable __function__))
  (and
   (mbe
      :logic (and (alistp x)
                  (equal (strip-cars x)
                         '(tag members flexiblep fixtype
                               recognizer fixer fixer-recognizer-thm
                               not-error-thm valuep-thm
                               value-kind-thm type-of-value-thm
                               flexiblep-thm type-to-quoted-thm
                               pointer-type-to-quoted-thm call)))
      :exec (fty::alist-with-carsp
                 x
                 '(tag members flexiblep fixtype
                       recognizer fixer fixer-recognizer-thm
                       not-error-thm valuep-thm
                       value-kind-thm type-of-value-thm
                       flexiblep-thm type-to-quoted-thm
                       pointer-type-to-quoted-thm call)))
   (b* ((tag (cdr (std::da-nth 0 x)))
        (members (cdr (std::da-nth 1 x)))
        (flexiblep (cdr (std::da-nth 2 x)))
        (fixtype (cdr (std::da-nth 3 x)))
        (recognizer (cdr (std::da-nth 4 x)))
        (fixer (cdr (std::da-nth 5 x)))
        (fixer-recognizer-thm (cdr (std::da-nth 6 x)))
        (not-error-thm (cdr (std::da-nth 7 x)))
        (valuep-thm (cdr (std::da-nth 8 x)))
        (value-kind-thm (cdr (std::da-nth 9 x)))
        (type-of-value-thm (cdr (std::da-nth 10 x)))
        (flexiblep-thm (cdr (std::da-nth 11 x)))
        (type-to-quoted-thm (cdr (std::da-nth 12 x)))
        (pointer-type-to-quoted-thm (cdr (std::da-nth 13 x)))
        (call (cdr (std::da-nth 14 x))))
     (and (identp tag)
          (defstruct-member-info-listp members)
          (booleanp flexiblep)
          (symbolp fixtype)
          (symbolp recognizer)
          (symbolp fixer)
          (symbolp fixer-recognizer-thm)
          (symbolp not-error-thm)
          (symbolp valuep-thm)
          (symbolp value-kind-thm)
          (symbolp type-of-value-thm)
          (symbolp flexiblep-thm)
          (symbolp type-to-quoted-thm)
          (symbolp pointer-type-to-quoted-thm)
          (pseudo-event-formp call))))))

Theorem: consp-when-defstruct-infop

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