		Search-engine friendly clone of the ACL2 documentation.

Processed-stv-p

Honsed-processed-stv

Raw constructor for honsed processed-stv-p structures.

Syntax:

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

This is identical to processed-stv, except that we hons the structure we are creating.

Definition

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

Function: honsed-processed-stv

(defun honsed-processed-stv
       (name user-stv compiled-stv relevant-signals)
 (declare (xargs :guard (and (symbolp name)
                             (compiled-stv-p compiled-stv))))
 (mbe
     :logic (processed-stv name
                           user-stv compiled-stv relevant-signals)
     :exec (hons :processed-stv
                 (hons (hons 'name name)
                       (hons (hons 'user-stv user-stv)
                             (hons (hons 'compiled-stv compiled-stv)
                                   (hons (hons 'relevant-signals
                                               relevant-signals)
                                         nil)))))))