		Search-engine friendly clone of the ACL2 documentation.

Account-statep

Make-account-state

Constructor macro for account-statep structures.

Syntax:

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

This is our preferred way to construct account-statep structures. It simply conses together a structure with the specified fields.

This macro generates a new account-statep structure from scratch. See also change-account-state, which can "change" an existing structure, instead.

The account-statep structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-account-state instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-account-state

(defmacro make-account-state (&rest args)
  (std::make-aggregate 'account-state
                       args
                       '((:nonce)
                         (:balance)
                         (:storage-root)
                         (:codehash))
                       'make-account-state
                       nil))