		Search-engine friendly clone of the ACL2 documentation.

Exprs-gin

Change-exprs-gin

Modifying constructor for exprs-gin structures.

Syntax

(change-exprs-gin x 
                  [:context <context>] 
                  [:inscope <inscope>] 
                  [:prec-tags <prec-tags>] 
                  [:fn <fn>] 
                  [:fn-guard <fn-guard>] 
                  [:compst-var <compst-var>] 
                  [:thm-index <thm-index>] 
                  [:names-to-avoid <names-to-avoid>] 
                  [:proofs <proofs>])

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

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

(defmacro change-exprs-gin (x &rest args)
  (std::change-aggregate
       'exprs-gin
       x args
       '((:context . exprs-gin->context)
         (:inscope . exprs-gin->inscope)
         (:prec-tags . exprs-gin->prec-tags)
         (:fn . exprs-gin->fn)
         (:fn-guard . exprs-gin->fn-guard)
         (:compst-var . exprs-gin->compst-var)
         (:thm-index . exprs-gin->thm-index)
         (:names-to-avoid . exprs-gin->names-to-avoid)
         (:proofs . exprs-gin->proofs))
       'change-exprs-gin
       'nil))