		Search-engine friendly clone of the ACL2 documentation.

Machine-statep

Change-machine-state

A copying macro that lets you create new machine-statep structures, based on existing structures.

Syntax:

(change-machine-state x 
                      [:gas-available <gas-available>] 
                      [:pc <pc>] 
                      [:memory <memory>] 
                      [:active-words <active-words>] 
                      [:stack <stack>])

This is a sometimes useful alternative to make-machine-state. It constructs a new machine-statep 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 std::defaggregate.

Macro: change-machine-state

(defmacro change-machine-state (x &rest args)
  (std::change-aggregate
       'machine-state
       x args
       '((:gas-available . machine-state->gas-available)
         (:pc . machine-state->pc)
         (:memory . machine-state->memory)
         (:active-words . machine-state->active-words)
         (:stack . machine-state->stack))
       'change-machine-state
       'nil))