		Search-engine friendly clone of the ACL2 documentation.

Pexprs-gin

Change-pexprs-gin

Modifying constructor for pexprs-gin structures.

Syntax

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

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

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