		Search-engine friendly clone of the ACL2 documentation.

Vl-atom

Change-vl-atom

Modifying constructor for vl-atom structures.

Syntax

(change-vl-atom x 
                [:guts <guts>] 
                [:finalwidth <finalwidth>] 
                [:finaltype <finaltype>] 
                [:atts <atts>])

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

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

(defmacro change-vl-atom (x &rest args)
  (std::change-aggregate 'vl-atom
                         x args
                         '((:guts . vl-atom->guts)
                           (:finalwidth . vl-atom->finalwidth)
                           (:finaltype . vl-atom->finaltype)
                           (:atts . vl-atom->atts))
                         'change-vl-atom
                         'remake-vl-atom))