		Search-engine friendly clone of the ACL2 documentation.

Compiled-stv-p

Make-compiled-stv

Constructor macro for compiled-stv-p structures.

Syntax:

(make-compiled-stv [: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 our preferred way to construct compiled-stv-p structures. It simply conses together a structure with the specified fields.

This macro generates a new compiled-stv-p structure from scratch. See also change-compiled-stv, which can "change" an existing structure, instead.

The compiled-stv-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-compiled-stv instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-compiled-stv

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