		Search-engine friendly clone of the ACL2 documentation.

Vls-data-p

Change-vls-data

A copying macro that lets you create new vls-data-p structures, based on existing structures.

Syntax:

(change-vls-data x 
                 [:good <good>] 
                 [:bad <bad>] 
                 [:orig <orig>] 
                 [:orig-descalist <orig-descalist>] 
                 [:filemap <filemap>] 
                 [:defs <defs>])

This is a sometimes useful alternative to make-vls-data. It constructs a new vls-data-p 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 defaggregate.

Macro: change-vls-data

(defmacro change-vls-data (x &rest args)
  (std::change-aggregate
       'vls-data
       x args
       '((:good . vls-data->good)
         (:bad . vls-data->bad)
         (:orig . vls-data->orig)
         (:orig-descalist . vls-data->orig-descalist)
         (:filemap . vls-data->filemap)
         (:defs . vls-data->defs))
       'change-vls-data
       'nil))