		Search-engine friendly clone of the ACL2 documentation.

Lstmt-gin

Change-lstmt-gin

Modifying constructor for lstmt-gin structures.

Syntax

(change-lstmt-gin x 
                  [:context <context>] 
                  [:typed-formals <typed-formals>] 
                  [:inscope <inscope>] 
                  [:fn <fn>] 
                  [:fn-guard <fn-guard>] 
                  [:compst-var <compst-var>] 
                  [:fenv-var <fenv-var>] 
                  [:limit-var <limit-var>] 
                  [:measure-for-fn <measure-for-fn>] 
                  [:measure-formals <measure-formals>] 
                  [: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-lstmt-gin.

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

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