		Search-engine friendly clone of the ACL2 documentation.

Account-statep

Make-honsed-account-state

Constructor macro for honsed account-statep structures.

Syntax:

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

This is identical to make-account-state, except that we hons the structure we are creating.

Definition

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

Macro: make-honsed-account-state

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