		Search-engine friendly clone of the ACL2 documentation.

Expr-gout

Change-expr-gout

Modifying constructor for expr-gout structures.

Syntax

(change-expr-gout x 
                  [:expr <expr>] 
                  [:type <type>] 
                  [:term <term>] 
                  [:events <events>] 
                  [:thm-name <thm-name>] 
                  [:thm-index <thm-index>] 
                  [:names-to-avoid <names-to-avoid>])

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

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

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