Change
Mutator macro for defrec structures.
The change macro is built into ACL2, and allows you to
"modify" instances of structures that have been introduced with defrec. Of course, since ACL2 is applicative, the original structure is not
actually changed—instead, a new structure is constructed, copying some
fields from the original structure and installing new values for other
fields.
For instance, suppose we first use make to create an employee
structure, e.g.,:
(defconst *jimmy* (make employee :name "Jimmy"
:salary 0
:position "Unpaid Intern")
Then we can use change to mutate this structure, e.g.,:
(change employee *jimmy* :salary 300000
:position "Vice President")
Produces a new employee structure where the name is still
"Jimmy", but where the salary and position have been updated to
300000 and "Vice President", respectively.
See defrec for more information.
