		Search-engine friendly clone of the ACL2 documentation.

Cstate

Change-cstate

Modifying constructor for cstate structures.

Syntax

(change-cstate x 
               [:local <local>])

This is an often useful alternative to make-cstate.

We construct a new cstate 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-cstate

(defmacro change-cstate (x &rest args)
  (std::change-aggregate 'cstate
                         x args '((:local . cstate->local))
                         'change-cstate
                         'nil))