		Search-engine friendly clone of the ACL2 documentation.

Processed-stv-p

Make-honsed-processed-stv

Constructor macro for honsed processed-stv-p structures.

Syntax:

(make-honsed-processed-stv [:name <name>] 
                           [:user-stv <user-stv>] 
                           [:compiled-stv <compiled-stv>] 
                           [:relevant-signals <relevant-signals>])

This is identical to make-processed-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-processed-stv

(defmacro make-honsed-processed-stv (&rest args)
  (std::make-aggregate 'processed-stv
                       args
                       '((:name)
                         (:user-stv)
                         (:compiled-stv)
                         (:relevant-signals))
                       'make-honsed-processed-stv
                       t))