		Search-engine friendly clone of the ACL2 documentation.

Exprs-gout

Change-exprs-gout

Modifying constructor for exprs-gout structures.

Syntax

(change-exprs-gout x 
                   [:exprs <exprs>] 
                   [:types <types>] 
                   [:terms <terms>] 
                   [:events <events>] 
                   [:thm-names <thm-names>] 
                   [:thm-index <thm-index>] 
                   [:names-to-avoid <names-to-avoid>])

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

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

(defmacro change-exprs-gout (x &rest args)
  (std::change-aggregate
       'exprs-gout
       x args
       '((:exprs . exprs-gout->exprs)
         (:types . exprs-gout->types)
         (:terms . exprs-gout->terms)
         (:events . exprs-gout->events)
         (:thm-names . exprs-gout->thm-names)
         (:thm-index . exprs-gout->thm-index)
         (:names-to-avoid . exprs-gout->names-to-avoid))
       'change-exprs-gout
       'nil))