		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>] 
                     [:reportcard <reportcard>] 
                     [:pstate <pstate>] 
                     [:filemap <filemap>])

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)
                           (:reportcard . vl-loadstate->reportcard)
                           (:pstate . vl-loadstate->pstate)
                           (:filemap . vl-loadstate->filemap))
                         'change-vl-loadstate
                         'remake-vl-loadstate))