		Search-engine friendly clone of the ACL2 documentation.

Vl-pp-opts-p

Vl-pp-opts

Raw constructor for vl-pp-opts-p structures.

Syntax:

(vl-pp-opts help readme output outdefs start-files 
            include-dirs defines edition strict mem)

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

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

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

Definition

This is an ordinary constructor function introduced by defaggregate.

Function: vl-pp-opts

(defun vl-pp-opts (help readme output outdefs start-files
                        include-dirs defines edition strict mem)
 (declare (xargs :guard (and (booleanp help)
                             (booleanp readme)
                             (stringp output)
                             (stringp outdefs)
                             (string-listp start-files)
                             (string-listp include-dirs)
                             (string-listp defines)
                             (vl-edition-p edition)
                             (booleanp strict)
                             (posp mem))))
 (cons
  :vl-pp-opts
  (cons
   (cons 'help help)
   (cons
    (cons 'readme readme)
    (cons
     (cons 'output output)
     (cons
      (cons 'outdefs outdefs)
      (cons
       (cons 'start-files start-files)
       (cons (cons 'include-dirs include-dirs)
             (cons (cons 'defines defines)
                   (cons (cons 'edition edition)
                         (cons (cons 'strict strict)
                               (cons (cons 'mem mem) nil))))))))))))