		Search-engine friendly clone of the ACL2 documentation.

Account-statep

Change-account-state

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

Syntax:

(change-account-state x 
                      [:nonce <nonce>] 
                      [:balance <balance>] 
                      [:storage-root <storage-root>] 
                      [:codehash <codehash>])

This is a sometimes useful alternative to make-account-state. It constructs a new account-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-account-state

(defmacro change-account-state (x &rest args)
  (std::change-aggregate
       'account-state
       x args
       '((:nonce . account-state->nonce)
         (:balance . account-state->balance)
         (:storage-root . account-state->storage-root)
         (:codehash . account-state->codehash))
       'change-account-state
       'nil))