		Search-engine friendly clone of the ACL2 documentation.

Jstatem-do

Change-jstatem-do

Modifying constructor for jstatem-do structures.

Syntax

(change-jstatem-do x 
                   [:body <body>] 
                   [:test <test>])

This is an often useful alternative to make-jstatem-do.

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

(defmacro change-jstatem-do (x &rest args)
  (std::change-aggregate 'jstatem-do
                         x args
                         '((:body . jstatem-do->body)
                           (:test . jstatem-do->test))
                         'change-jstatem-do
                         'nil))