		Search-engine friendly clone of the ACL2 documentation.

Stmt-gout

Change-stmt-gout

Modifying constructor for stmt-gout structures.

Syntax

(change-stmt-gout x 
                  [:items <items>] 
                  [:type <type>] 
                  [:term <term>] 
                  [:context <context>] 
                  [:inscope <inscope>] 
                  [:limit <limit>] 
                  [:events <events>] 
                  [:thm-name <thm-name>] 
                  [:thm-index <thm-index>] 
                  [:names-to-avoid <names-to-avoid>])

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

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

(defmacro change-stmt-gout (x &rest args)
  (std::change-aggregate
       'stmt-gout
       x args
       '((:items . stmt-gout->items)
         (:type . stmt-gout->type)
         (:term . stmt-gout->term)
         (:context . stmt-gout->context)
         (:inscope . stmt-gout->inscope)
         (:limit . stmt-gout->limit)
         (:events . stmt-gout->events)
         (:thm-name . stmt-gout->thm-name)
         (:thm-index . stmt-gout->thm-index)
         (:names-to-avoid . stmt-gout->names-to-avoid))
       'change-stmt-gout
       'nil))