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