		Search-engine friendly clone of the ACL2 documentation.

Pexprs-gout

Change-pexprs-gout

Modifying constructor for pexprs-gout structures.

Syntax

(change-pexprs-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-pexprs-gout.

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

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