		Search-engine friendly clone of the ACL2 documentation.

Compiled-stv-p

Make-honsed-compiled-stv

Constructor macro for honsed compiled-stv-p structures.

Syntax:

(make-honsed-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 identical to make-compiled-stv, except that we hons the structure we are creating.

Definition

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

Macro: make-honsed-compiled-stv

(defmacro make-honsed-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-honsed-compiled-stv
                       t))