		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))