		Search-engine friendly clone of the ACL2 documentation.

Stmt-gin

Change-stmt-gin

Modifying constructor for stmt-gin structures.

Syntax

(change-stmt-gin x 
                 [:context <context>] 
                 [:var-term-alist <var-term-alist>] 
                 [:typed-formals <typed-formals>] 
                 [:inscope <inscope>] 
                 [:loop-flag <loop-flag>] 
                 [:affect <affect>] 
                 [:fn <fn>] 
                 [:fn-guard <fn-guard>] 
                 [:compst-var <compst-var>] 
                 [:fenv-var <fenv-var>] 
                 [:limit-var <limit-var>] 
                 [:prec-fns <prec-fns>] 
                 [:prec-tags <prec-tags>] 
                 [:prec-objs <prec-objs>] 
                 [:thm-index <thm-index>] 
                 [:names-to-avoid <names-to-avoid>] 
                 [:proofs <proofs>])

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

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

(defmacro change-stmt-gin (x &rest args)
  (std::change-aggregate
       'stmt-gin
       x args
       '((:context . stmt-gin->context)
         (:var-term-alist . stmt-gin->var-term-alist)
         (:typed-formals . stmt-gin->typed-formals)
         (:inscope . stmt-gin->inscope)
         (:loop-flag . stmt-gin->loop-flag)
         (:affect . stmt-gin->affect)
         (:fn . stmt-gin->fn)
         (:fn-guard . stmt-gin->fn-guard)
         (:compst-var . stmt-gin->compst-var)
         (:fenv-var . stmt-gin->fenv-var)
         (:limit-var . stmt-gin->limit-var)
         (:prec-fns . stmt-gin->prec-fns)
         (:prec-tags . stmt-gin->prec-tags)
         (:prec-objs . stmt-gin->prec-objs)
         (:thm-index . stmt-gin->thm-index)
         (:names-to-avoid . stmt-gin->names-to-avoid)
         (:proofs . stmt-gin->proofs))
       'change-stmt-gin
       'nil))