		Search-engine friendly clone of the ACL2 documentation.

Processed-stv-p

Make-processed-stv

Constructor macro for processed-stv-p structures.

Syntax:

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

This is our preferred way to construct processed-stv-p structures. It simply conses together a structure with the specified fields.

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

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

Definition

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

Macro: make-processed-stv

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