		Search-engine friendly clone of the ACL2 documentation.

Lstmt-gout

Change-lstmt-gout

Modifying constructor for lstmt-gout structures.

Syntax

(change-lstmt-gout x 
                   [:stmt <stmt>] 
                   [:test-term <test-term>] 
                   [:body-term <body-term>] 
                   [:affect <affect>] 
                   [:limit-body <limit-body>] 
                   [:limit-all <limit-all>] 
                   [:events <events>] 
                   [:thm-name <thm-name>] 
                   [:thm-index <thm-index>] 
                   [:names-to-avoid <names-to-avoid>])

This is an often useful alternative to make-lstmt-gout.

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

(defmacro change-lstmt-gout (x &rest args)
  (std::change-aggregate
       'lstmt-gout
       x args
       '((:stmt . lstmt-gout->stmt)
         (:test-term . lstmt-gout->test-term)
         (:body-term . lstmt-gout->body-term)
         (:affect . lstmt-gout->affect)
         (:limit-body . lstmt-gout->limit-body)
         (:limit-all . lstmt-gout->limit-all)
         (:events . lstmt-gout->events)
         (:thm-name . lstmt-gout->thm-name)
         (:thm-index . lstmt-gout->thm-index)
         (:names-to-avoid . lstmt-gout->names-to-avoid))
       'change-lstmt-gout
       'nil))