		Search-engine friendly clone of the ACL2 documentation.

Compiled-stv-p

Change-compiled-stv

A copying macro that lets you create new compiled-stv-p structures, based on existing structures.

Syntax:

(change-compiled-stv x 
                     [:nphases <nphases>] 
                     [:nst-extract-alists <nst-extract-alists>] 
                     [:out-extract-alists <out-extract-alists>] 
                     [:int-extract-alists <int-extract-alists>] 
                     [:override-bits <override-bits>] 
                     [:restrict-alist <restrict-alist>] 
                     [:in-usersyms <in-usersyms>] 
                     [:out-usersyms <out-usersyms>] 
                     [:expanded-ins <expanded-ins>] 
                     [:override-paths <override-paths>])

This is a sometimes useful alternative to make-compiled-stv. It constructs a new compiled-stv-p 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 std::defaggregate.

Macro: change-compiled-stv

(defmacro
     change-compiled-stv (x &rest args)
     (std::change-aggregate
          'compiled-stv
          x args
          '((:nphases . compiled-stv->nphases)
            (:nst-extract-alists . compiled-stv->nst-extract-alists)
            (:out-extract-alists . compiled-stv->out-extract-alists)
            (:int-extract-alists . compiled-stv->int-extract-alists)
            (:override-bits . compiled-stv->override-bits)
            (:restrict-alist . compiled-stv->restrict-alist)
            (:in-usersyms . compiled-stv->in-usersyms)
            (:out-usersyms . compiled-stv->out-usersyms)
            (:expanded-ins . compiled-stv->expanded-ins)
            (:override-paths . compiled-stv->override-paths))
          'change-compiled-stv
          'nil))