		Search-engine friendly clone of the ACL2 documentation.

Compiled-stv-p

Honsed-compiled-stv

Raw constructor for honsed compiled-stv-p structures.

Syntax:

(honsed-compiled-stv nphases 
                     nst-extract-alists out-extract-alists 
                     int-extract-alists override-bits 
                     restrict-alist in-usersyms out-usersyms 
                     expanded-ins override-paths)

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

Definition

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

Function: honsed-compiled-stv

(defun honsed-compiled-stv
       (nphases nst-extract-alists out-extract-alists
                int-extract-alists override-bits
                restrict-alist in-usersyms out-usersyms
                expanded-ins override-paths)
 (declare (xargs :guard (and (posp nphases)
                             (true-listp nst-extract-alists)
                             (true-listp out-extract-alists)
                             (true-listp int-extract-alists)
                             (symbol-listp override-bits)
                             (true-listp override-paths))))
 (mbe
  :logic (compiled-stv nphases
                       nst-extract-alists out-extract-alists
                       int-extract-alists override-bits
                       restrict-alist in-usersyms out-usersyms
                       expanded-ins override-paths)
  :exec
  (hons
   :compiled-stv
   (hons
    (hons 'nphases nphases)
    (hons
     (hons 'nst-extract-alists
           nst-extract-alists)
     (hons
      (hons 'out-extract-alists
            out-extract-alists)
      (hons
       (hons 'int-extract-alists
             int-extract-alists)
       (hons
        (hons 'override-bits override-bits)
        (hons
         (hons 'restrict-alist restrict-alist)
         (hons
             (hons 'in-usersyms in-usersyms)
             (hons (hons 'out-usersyms out-usersyms)
                   (hons (hons 'expanded-ins expanded-ins)
                         (hons (hons 'override-paths override-paths)
                               nil)))))))))))))