		Search-engine friendly clone of the ACL2 documentation.

Defstruct-member-info

Make-defstruct-member-info

Basic constructor macro for defstruct-member-info structures.

Syntax

(make-defstruct-member-info [:memtype <memtype>] 
                            [:reader <reader>] 
                            [:reader-element <reader-element>] 
                            [:writer <writer>] 
                            [:writer-element <writer-element>] 
                            [:checker <checker>] 
                            [:length <length>] 
                            [:reader-return-thm <reader-return-thm>] 
                            [:reader-element-return-thm <reader-element-return-thm>] 
                            [:writer-return-thm <writer-return-thm>] 
                            [:writer-element-return-thm <writer-element-return-thm>])

This is the usual way to construct defstruct-member-info structures. It simply conses together a structure with the specified fields.

This macro generates a new defstruct-member-info structure from scratch. See also change-defstruct-member-info, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-defstruct-member-info

(defmacro make-defstruct-member-info (&rest args)
  (std::make-aggregate 'defstruct-member-info
                       args
                       '((:memtype)
                         (:reader)
                         (:reader-element)
                         (:writer)
                         (:writer-element)
                         (:checker)
                         (:length)
                         (:reader-return-thm)
                         (:reader-element-return-thm)
                         (:writer-return-thm)
                         (:writer-element-return-thm))
                       'make-defstruct-member-info
                       nil))

Function: defstruct-member-info

(defun defstruct-member-info
       (memtype reader
                reader-element writer writer-element
                checker length reader-return-thm
                reader-element-return-thm
                writer-return-thm
                writer-element-return-thm)
 (declare (xargs :guard (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))))
 (declare (xargs :guard t))
 (let ((__function__ 'defstruct-member-info))
  (declare (ignorable __function__))
  (b* ((memtype (mbe :logic (member-type-fix memtype)
                     :exec memtype))
       (reader (mbe :logic (symbol-fix reader)
                    :exec reader))
       (reader-element (mbe :logic (symbol-fix reader-element)
                            :exec reader-element))
       (writer (mbe :logic (symbol-fix writer)
                    :exec writer))
       (writer-element (mbe :logic (symbol-fix writer-element)
                            :exec writer-element))
       (checker (mbe :logic (symbol-fix checker)
                     :exec checker))
       (length (mbe :logic (symbol-fix length)
                    :exec length))
       (reader-return-thm (mbe :logic (symbol-fix reader-return-thm)
                               :exec reader-return-thm))
       (reader-element-return-thm
            (mbe :logic (symbol-fix reader-element-return-thm)
                 :exec reader-element-return-thm))
       (writer-return-thm (mbe :logic (symbol-fix writer-return-thm)
                               :exec writer-return-thm))
       (writer-element-return-thm
            (mbe :logic (symbol-fix writer-element-return-thm)
                 :exec writer-element-return-thm)))
    (list (cons 'memtype memtype)
          (cons 'reader reader)
          (cons 'reader-element reader-element)
          (cons 'writer writer)
          (cons 'writer-element writer-element)
          (cons 'checker checker)
          (cons 'length length)
          (cons 'reader-return-thm
                reader-return-thm)
          (cons 'reader-element-return-thm
                reader-element-return-thm)
          (cons 'writer-return-thm
                writer-return-thm)
          (cons 'writer-element-return-thm
                writer-element-return-thm)))))