		Search-engine friendly clone of the ACL2 documentation.

Machine-statep

Make-honsed-machine-state

Constructor macro for honsed machine-statep structures.

Syntax:

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

This is identical to make-machine-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-machine-state

(defmacro make-honsed-machine-state (&rest args)
  (std::make-aggregate 'machine-state
                       args
                       '((:gas-available)
                         (:pc)
                         (:memory)
                         (:active-words)
                         (:stack))
                       'make-honsed-machine-state
                       t))