		Search-engine friendly clone of the ACL2 documentation.

Stmt-switch

Change-stmt-switch

Modifying constructor for stmt-switch structures.

Syntax

(change-stmt-switch x 
                    [:ctrl <ctrl>] 
                    [:body <body>])

This is an often useful alternative to make-stmt-switch.

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

(defmacro change-stmt-switch (x &rest args)
  (std::change-aggregate 'stmt-switch
                         x args
                         '((:ctrl . stmt-switch->ctrl)
                           (:body . stmt-switch->body))
                         'change-stmt-switch
                         'nil))