		Search-engine friendly clone of the ACL2 documentation.

System-state

Change-system-state

Modifying constructor for system-state structures.

Syntax

(change-system-state x 
                     [:validators <validators>] 
                     [:network <network>])

This is an often useful alternative to make-system-state.

We construct a new system-state 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 fty::defprod.

Macro: change-system-state

(defmacro change-system-state (x &rest args)
  (std::change-aggregate 'system-state
                         x args
                         '((:validators . system-state->validators)
                           (:network . system-state->network))
                         'change-system-state
                         'nil))