		Search-engine friendly clone of the ACL2 documentation.

Struct-declon-member

Change-struct-declon-member

Modifying constructor for struct-declon-member structures.

Syntax

(change-struct-declon-member x 
                             [:extension <extension>] 
                             [:specquals <specquals>] 
                             [:declors <declors>] 
                             [:attribs <attribs>])

This is an often useful alternative to make-struct-declon-member.

We construct a new struct-declon-member 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-struct-declon-member

(defmacro change-struct-declon-member (x &rest args)
  (std::change-aggregate
       'struct-declon-member
       x args
       '((:extension . struct-declon-member->extension)
         (:specquals . struct-declon-member->specquals)
         (:declors . struct-declon-member->declors)
         (:attribs . struct-declon-member->attribs))
       'change-struct-declon-member
       'remake-struct-declon-member))