		Search-engine friendly clone of the ACL2 documentation.

Sdm-instruction-table-entry

Change-sdm-instruction-table-entry

Modifying constructor for sdm-instruction-table-entry structures.

Syntax

(change-sdm-instruction-table-entry x 
                                    [:title <title>] 
                                    [:implemented <implemented>] 
                                    [:unimplemented <unimplemented>] 
                                    [:doc <doc>] 
                                    [:subsecs <subsecs>])

This is an often useful alternative to make-sdm-instruction-table-entry.

We construct a new sdm-instruction-table-entry 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 defprod.

Macro: change-sdm-instruction-table-entry

(defmacro change-sdm-instruction-table-entry (x &rest args)
  (std::change-aggregate
       'sdm-instruction-table-entry
       x args
       '((:title . sdm-instruction-table-entry->title)
         (:implemented .
                       sdm-instruction-table-entry->implemented)
         (:unimplemented .
                         sdm-instruction-table-entry->unimplemented)
         (:doc . sdm-instruction-table-entry->doc)
         (:subsecs . sdm-instruction-table-entry->subsecs))
       'change-sdm-instruction-table-entry
       'nil))