		Search-engine friendly clone of the ACL2 documentation.

Stv2c-opts-p

Honsed-stv2c-opts

Raw constructor for honsed stv2c-opts-p structures.

Syntax:

(honsed-stv2c-opts help readme stv start-files search-path 
                   search-exts defines edition strict mem)

This is identical to stv2c-opts, except that we hons the structure we are creating.

Definition

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

Function: honsed-stv2c-opts

(defun honsed-stv2c-opts
       (help readme stv start-files search-path
             search-exts defines edition strict mem)
 (declare (xargs :guard (and (booleanp help)
                             (booleanp readme)
                             (stringp stv)
                             (string-listp start-files)
                             (string-listp search-path)
                             (string-listp search-exts)
                             (string-listp defines)
                             (vl2014::vl-edition-p edition)
                             (booleanp strict)
                             (posp mem))))
 (mbe
  :logic (stv2c-opts help readme stv start-files search-path
                     search-exts defines edition strict mem)
  :exec
  (hons
   :stv2c-opts
   (hons
    (hons 'help help)
    (hons
     (hons 'readme readme)
     (hons
      (hons 'stv stv)
      (hons
       (hons 'start-files start-files)
       (hons
        (hons 'search-path search-path)
        (hons
            (hons 'search-exts search-exts)
            (hons (hons 'defines defines)
                  (hons (hons 'edition edition)
                        (hons (hons 'strict strict)
                              (hons (hons 'mem mem) nil)))))))))))))