		Search-engine friendly clone of the ACL2 documentation.

Processed-stv-p

Processed-stv

Raw constructor for processed-stv-p structures.

Syntax:

(processed-stv name 
               user-stv compiled-stv relevant-signals)

This is the lowest-level constructor for processed-stv-p structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-processed-stv or change-processed-stv instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

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

Definition

This is an ordinary constructor function introduced by std::defaggregate.

Function: processed-stv

(defun processed-stv (name user-stv compiled-stv relevant-signals)
 (declare (xargs :guard (and (symbolp name)
                             (compiled-stv-p compiled-stv))))
 (cons
  :processed-stv (cons (cons 'name name)
                       (cons (cons 'user-stv user-stv)
                             (cons (cons 'compiled-stv compiled-stv)
                                   (cons (cons 'relevant-signals
                                               relevant-signals)
                                         nil))))))