		Search-engine friendly clone of the ACL2 documentation.

Stv2c-opts-p

Stv2c-opts

Raw constructor for stv2c-opts-p structures.

Syntax:

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

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

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

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

Definition

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

Function: stv2c-opts

(defun 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))))
 (cons
  :stv2c-opts
  (cons
   (cons 'help help)
   (cons
    (cons 'readme readme)
    (cons
     (cons 'stv stv)
     (cons
      (cons 'start-files start-files)
      (cons
       (cons 'search-path search-path)
       (cons (cons 'search-exts search-exts)
             (cons (cons 'defines defines)
                   (cons (cons 'edition edition)
                         (cons (cons 'strict strict)
                               (cons (cons 'mem mem) nil))))))))))))