		Search-engine friendly clone of the ACL2 documentation.

Substatep

Change-substate

A copying macro that lets you create new substatep structures, based on existing structures.

Syntax:

(change-substate x 
                 [:self-destruct-set <self-destruct-set>] 
                 [:log-series <log-series>] 
                 [:touched-accounts <touched-accounts>] 
                 [:refund-balance <refund-balance>])

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

(defmacro change-substate (x &rest args)
  (std::change-aggregate
       'substate
       x args
       '((:self-destruct-set . substate->self-destruct-set)
         (:log-series . substate->log-series)
         (:touched-accounts . substate->touched-accounts)
         (:refund-balance . substate->refund-balance))
       'change-substate
       'nil))