		Search-engine friendly clone of the ACL2 documentation.

Defstruct-member-info

Change-defstruct-member-info

Modifying constructor for defstruct-member-info structures.

Syntax

(change-defstruct-member-info x 
                              [: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 an often useful alternative to make-defstruct-member-info.

We construct a new defstruct-member-info structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-defstruct-member-info

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