		Search-engine friendly clone of the ACL2 documentation.

Vl-loadstate

Change-vl-loadstate

Modifying constructor for vl-loadstate structures.

Syntax

(change-vl-loadstate x 
                     [:config <config>] 
                     [:descs <descs>] 
                     [:descalist <descalist>] 
                     [:defines <defines>] 
                     [:iskips <iskips>] 
                     [:ifdefmap <ifdefmap>] 
                     [:defmap <defmap>] 
                     [:idcache <idcache>] 
                     [:spcache <spcache>] 
                     [:reportcard <reportcard>] 
                     [:pstate <pstate>] 
                     [:filemap <filemap>] 
                     [:bytes <bytes>])

This is an often useful alternative to make-vl-loadstate.

We construct a new vl-loadstate 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-vl-loadstate

(defmacro change-vl-loadstate (x &rest args)
  (std::change-aggregate 'vl-loadstate
                         x args
                         '((:config . vl-loadstate->config)
                           (:descs . vl-loadstate->descs)
                           (:descalist . vl-loadstate->descalist)
                           (:defines . vl-loadstate->defines)
                           (:iskips . vl-loadstate->iskips)
                           (:ifdefmap . vl-loadstate->ifdefmap)
                           (:defmap . vl-loadstate->defmap)
                           (:idcache . vl-loadstate->idcache)
                           (:spcache . vl-loadstate->spcache)
                           (:reportcard . vl-loadstate->reportcard)
                           (:pstate . vl-loadstate->pstate)
                           (:filemap . vl-loadstate->filemap)
                           (:bytes . vl-loadstate->bytes))
                         'change-vl-loadstate
                         'remake-vl-loadstate))