		Search-engine friendly clone of the ACL2 documentation.

Expr-gin

Change-expr-gin

Modifying constructor for expr-gin structures.

Syntax

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

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

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