|
|
|---|
|
|
|
|---|
Raw constructor for honsed substatep structures.
Syntax:
(honsed-substate self-destruct-set log-series
touched-accounts refund-balance)This is identical to substate, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-substate (self-destruct-set log-series touched-accounts refund-balance) (declare (xargs :guard (and (all-addressp self-destruct-set) (all-addressp touched-accounts) (weip refund-balance)))) (mbe :logic (substate self-destruct-set log-series touched-accounts refund-balance) :exec (hons (hons 'self-destruct-set self-destruct-set) (hons (hons 'log-series log-series) (hons (hons 'touched-accounts touched-accounts) (hons (hons 'refund-balance refund-balance) nil))))))