		Search-engine friendly clone of the ACL2 documentation.

Vl-lintconfig-p

Vl-lintconfig

Raw constructor for vl-lintconfig-p structures.

Syntax:

(vl-lintconfig start-files plusargs 
               help readme search-path search-exts 
               include-dirs topmods quiet dropmods 
               ignore ignore-files defines cclimit 
               global-packages elab-limit stmt-limit 
               no-typo no-html no-sv-use-set edition 
               strict mem debug shell post-shell)

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

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

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

Definition

This is an ordinary constructor function introduced by defaggregate.

Function: vl-lintconfig

(defun vl-lintconfig
       (start-files plusargs
                    help readme search-path search-exts
                    include-dirs topmods quiet dropmods
                    ignore ignore-files defines cclimit
                    global-packages elab-limit stmt-limit
                    no-typo no-html no-sv-use-set edition
                    strict mem debug shell post-shell)
 (declare (xargs :guard (and (string-listp start-files)
                             (string-listp plusargs)
                             (booleanp help)
                             (booleanp readme)
                             (string-listp search-path)
                             (string-listp search-exts)
                             (string-listp include-dirs)
                             (string-listp topmods)
                             (string-listp quiet)
                             (string-listp dropmods)
                             (string-listp ignore)
                             (string-listp ignore-files)
                             (string-listp defines)
                             (natp cclimit)
                             (string-listp global-packages)
                             (natp elab-limit)
                             (natp stmt-limit)
                             (booleanp no-typo)
                             (booleanp no-html)
                             (booleanp no-sv-use-set)
                             (vl-edition-p edition)
                             (booleanp strict)
                             (posp mem)
                             (booleanp debug)
                             (booleanp shell)
                             (booleanp post-shell))))
 (cons
     :vl-lint-opts
     (cons (cons (cons (cons start-files (cons plusargs help))
                       (cons readme (cons search-path search-exts)))
                 (cons (cons include-dirs (cons topmods quiet))
                       (cons (cons dropmods ignore)
                             (cons ignore-files defines))))
           (cons (cons (cons cclimit
                             (cons global-packages elab-limit))
                       (cons stmt-limit (cons no-typo no-html)))
                 (cons (cons no-sv-use-set (cons edition strict))
                       (cons (cons mem debug)
                             (cons shell post-shell)))))))